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.