Hola.
Respecto a lo primero, tenés que usar comas para separar en análisis entre las dos variables, sino entiende que es una aplicación (por eso el mensaje de error, ya que true o false no esperan argumentos; no son funciones):
...
match b1, b2 with
| false, false => false
...
Respecto a lo segundo, Fixpoint chequea que un argumento se achique estructuralmente (tenga menos constructores en cada llamado recursivo). Por defecto lo hace sobre el último argumento pero esto podés precisarlo (vero el teórico, función suma de naturales). En este caso se cumple que en el llamado recursivo el segundo argumento es más peque~no (tiene un sucesor menos). Hay un caso base que está mal si lo que querés definir es "menor o igual", ya que 0<=0. Esta función se puede definir en menos casos.
Saludos, Carlos