Library denumerable.Arith_lemmas
Require Import Even.
Require Import Div2.
Require Import Omega.
Section Arith_lemmas.
Lemma nat_double_or_s_double :
forall n, {exists p, n = double p} + {exists p, n = S (double p)}.
Proof.
induction n.
apply left.
exists 0; auto with arith.
induction IHn.
apply right.
destruct a.
exists x.
auto.
apply left.
destruct b.
exists (S x).
rewrite H.
symmetry; apply double_S.
Qed.
Lemma div2_double_is_id :
forall n : nat, div2 (double n) = n.
Proof.
intro n.
induction n.
replace (double 0) with 0; auto.
replace (double (S n)) with (S (S (double n))).
replace (S n) with (S (div2 (double n))); auto.
symmetry; apply double_S.
Qed.
Lemma double_inj :
forall (m n : nat), double m = double n -> m = n.
Proof.
intros m n double_eq.
unfold double in double_eq.
omega.
Qed.
Lemma double_is_even :
forall n : nat, even (double n).
Proof.
intro n.
induction n.
replace (double 0) with 0.
apply even_O.
auto.
replace (double (S n)) with (S (S (double n))).
apply even_S.
apply odd_S.
assumption.
symmetry.
apply double_S.
Qed.
Lemma not_double_is_s_double :
forall (m n : nat), ~ (S (double m) = double n).
Proof.
intros m n eq.
apply (not_even_and_odd (double n)).
apply double_is_even.
rewrite <- eq.
apply odd_S.
apply double_is_even.
Qed.
Lemma even_prod :
forall p q, even ((p + q + 1) * (p + q)).
Proof.
intros p q.
case (even_odd_dec (p + q)).
intro Hev; apply even_mult_r; assumption.
intro Hod; apply even_mult_l; replace (p + q + 1) with (S (p + q)).
apply even_S; assumption.
omega.
Qed.
Lemma plus_2 :
forall n, S (S n) = n + 2.
Proof.
intro n.
replace 2 with (1 + 1).
rewrite (plus_assoc n 1 1).
cut (forall m, S m = m + 1).
intro H.
replace (S n) with (n + 1); auto with arith.
intro m; rewrite (plus_comm m 1); auto with arith.
auto with arith.
Qed.
End Arith_lemmas.