fixed lemma Full in int.NumOfParam (thanks to F. Pottier)

parent 616f63a3
......@@ -281,7 +281,7 @@ theory NumOfParam
(* by induction on b *)
lemma Full :
forall p : param, a b : int. a < b ->
forall p : param, a b : int. a <= b ->
(forall n : int. a <= n < b -> pr p n) -> num_of p a b = b - a
(* by induction on b *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment