proposition: Lemma even_odd_cor : forall n:nat, exists p : nat, n = (2 * p)%nat \/ n = S (2 * p).
proof: Proof. intros n; exists (Nat.div2 n). case_eq (Nat.odd n); intros H; [right|left]. - assert (Nat.b2n (Nat.odd n) = 1%nat) as Hb by now rewrite H. rewrite Nat.div2_odd at 1; rewrite Hb, Nat.add_1_r; reflexivity. - assert (Nat.b2n (Nat.odd n) = 0%nat) as Hb by now rewrite H. rewrite Nat.div2_odd at 1; rewrite Hb, Nat.add_0_r; reflexivity. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun ArithRing