Commit 185b87df authored by MARCHE Claude's avatar MARCHE Claude

fix realization of number.Parity

parent 5ebaf514
......@@ -123,3 +123,14 @@ intros k.
now exists k.
Qed.
(* Why3 goal *)
Lemma even_mod2 : forall (n:Z), (even n) <->
((ZArith.BinInt.Z.rem n 2%Z) = 0%Z).
Proof.
intros n.
rewrite even_is_Zeven.
rewrite <- Zeven_bool_iff.
rewrite Zquot.Zeven_rem.
now rewrite Z.eqb_eq.
Qed.
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