Fstar says "An unknown assertion in the term at this location was not provable"?

range.fst

module Range

val length: list 'a -> Tot nat
let rec length l =
	match l with
	| [] -> 0
	| _::tl -> 1 + length tl

val range: a:nat -> b:nat -> Tot (list nat)
			(decreases (b-a))
let rec range a b =
	if b-a <= 0
	then []
	else a :: (range (a+1) b)

(*
 induction_hyp := length (range (a+1) b) = b-(a+1)+1

 length (range a b)
 = length (a :: (range (a+1) b))	(range)
 = 1 + length (range (a+1) b)		(length)
 = 1 + b-a							(induction_hyp)
*)
val range_correctness: a:nat -> b:nat{b>=a}
		-> Lemma (length (range a b) = b-a+1)
			(decreases (b-a))
let rec range_correctness a b =
	if b-a = 0
	then ()
	else range_correctness (a+1) b


(* my fstar(fdbbead) says:
Error range.fst(27,0-30,31): An unknown assertion in the term at this location w
as not provable
Verified module: Prims
Verified module: Range
Error: 1 errors were reported (see above)

*)

I've finally found L25 "b-a+1" interpreted as "b-(a+1)" (right associative!?!?!!?!???!!!!).