# Library Circuits.GENE.Arith_compl

Require Export Plus.
Require Export Mult.
Require Import Minus.
Require Export Lt.
Require Export Le.
Require Export Gt.

Lemma plus_n_SO : forall x : nat, x + 1 = S x.
intros; rewrite plus_comm; auto with v62.
Qed. Hint Resolve plus_n_SO.

Lemma plus_permute2 : forall x y z : nat, x + y + z = x + z + y.
intros.
rewrite (plus_comm x y).
rewrite (plus_comm x z).
rewrite plus_comm.
symmetry in |- *.
rewrite plus_comm.
rewrite plus_permute.
auto with v62.
Qed. Hint Resolve plus_permute2.

Lemma mult_sym : forall a b : nat, a * b = b * a.
intros a b; elim a; simpl in |- *; auto with v62.
intros y H.
replace (y * b) with (b * y).
elim (mult_n_Sm b y).
apply plus_comm.
Qed. Hint Resolve mult_sym.

Lemma mult_permute : forall a b c : nat, a * b * c = a * c * b.
intros.
rewrite mult_assoc_reverse.
rewrite mult_assoc_reverse.
replace (c * b) with (b * c); auto with v62.
Qed. Hint Resolve mult_permute.

Lemma plus_O_O : forall n m : nat, n + m = 0 -> n = 0.
simple induction n. intros. trivial with v62.
intros. inversion H0.
Qed.

Lemma mult_plus_distr2 : forall n m p : nat, n * (m + p) = n * m + n * p.
intros. rewrite mult_sym. rewrite mult_plus_distr_r. rewrite mult_sym.
replace (p * n) with (n * p). trivial with v62. apply mult_sym.
Qed.

Fixpoint power2 (n : nat) : nat :=
match n with
| O => 1
| S x => power2 x + power2 x
end.

Lemma power2_eq2 : forall x : nat, power2 (S x) = power2 x + power2 x.
Proof.
auto with v62.
Qed.

Lemma power2_plus : forall x y : nat, power2 (x + y) = power2 x * power2 y.
simple induction x. intros. simpl in |- *. elim plus_n_O; auto with v62.
intros. simpl in |- *. rewrite H. rewrite mult_plus_distr_r. trivial with v62.
Qed.

Theorem le_plus_n_m : forall n m : nat, n <= m -> n + n <= m + m.
simple induction n. auto with v62.
intros. inversion H0. auto with v62.
simpl in |- *. elim plus_n_Sm. elim plus_n_Sm.
apply le_n_S. apply le_n_S. apply H. apply le_Sn_le. exact H1.
Qed. Hint Resolve le_plus_n_m.

Theorem lt_plus_n_m : forall n m : nat, n < m -> S (n + n) < m + m.
simple induction n.
simpl in |- *. simple induction m. simpl in |- *. intros. absurd (0 < 0). apply le_not_lt. auto with v62.
exact H.
intros. simpl in |- *. elim plus_n_Sm. apply lt_n_S. auto with v62.
intros. inversion H0. simpl in |- *. repeat elim plus_n_Sm. auto with v62.
simpl in |- *.
repeat elim plus_n_Sm. apply lt_n_S. apply lt_n_S. apply H. inversion H1. auto with v62.
apply le_lt_n_Sm. apply le_Sn_le. apply le_Sn_le. exact H3.
Qed.

Lemma le_plus_lem1 : forall a b c : nat, a <= b -> c + a <= c + b.
intros. inversion H. auto with v62.
elim plus_n_Sm. apply le_S. auto with v62.
Qed. Hint Resolve le_plus_lem1.

Lemma le_plus_lem2 : forall a b c : nat, c + a <= c + b -> a <= b.
simple induction c. auto with v62.
simpl in |- *. intros. apply H. apply le_S_n. exact H0.
Qed.

Lemma gt_double : forall a b : nat, a + a > b + b -> a > b.
simple induction a. simpl in |- *. intros. absurd (0 > b + b). auto with v62.
auto with v62. simple induction b. simpl in |- *. auto with v62.
intros. apply gt_n_S.
apply H. generalize H1. simpl in |- *. elim plus_n_Sm. elim plus_n_Sm. intro.
cut (S (n + n) > S (n0 + n0)). intro. apply gt_S_n. exact H3.
apply gt_S_n. exact H2.
Qed.

Lemma gt_double_inv : forall a b : nat, a > b -> a + a > b + b.
simple induction a. intros. absurd (0 > b). auto with v62. exact H.
simple induction b. intros. simpl in |- *. auto with v62.
intros. simpl in |- *. elim plus_n_Sm.
elim plus_n_Sm. apply gt_n_S. apply gt_n_S. apply H. apply gt_S_n. exact H1.
Qed.

Lemma gt_double_n_S : forall a b : nat, a > b -> a + a > S (b + b).
simple induction a. intros. absurd (0 > b). auto with v62.
exact H.
simple induction b. simpl in |- *. intro.
apply gt_n_S. unfold gt in |- *. unfold lt in |- *. elim plus_n_Sm. auto with v62.
intros. simpl in |- *. apply gt_n_S.
elim plus_n_Sm. apply gt_n_S. elim plus_n_Sm. apply H. apply gt_S_n. exact H1.
Qed.

Lemma gt_double_S_n : forall a b : nat, a > b -> S (a + a) > b + b.
intros. apply gt_trans with (a + a). auto with v62. apply gt_double_inv. exact H.
Qed.

Lemma minus_le_O : forall a b : nat, a <= b -> a - b = 0.
intros. pattern a, b in |- *. apply le_elim_rel. auto with v62.
intros. simpl in |- *. exact H1.
exact H.
Qed.

Lemma minus_n_SO : forall n : nat, n - 1 = pred n.
simple induction n. auto with v62. intros. simpl in |- *. auto with v62.
Qed.

Lemma minus_le_lem2c : forall a b : nat, a - S b <= a - b.
intros. pattern a, b in |- *. apply nat_double_ind. auto with v62.
intro. elim minus_n_O. rewrite minus_n_SO. simpl in |- *. auto with v62.
intros. simpl in |- *. exact H.
Qed.

Lemma minus_le_lem2 : forall a b : nat, a - b <= a.
simple induction b. elim minus_n_O. auto with v62.
intros. apply le_trans with (a - n). apply minus_le_lem2c.
exact H.
Qed. Hint Resolve minus_le_lem2.

Lemma minus_minus_lem1 : forall a b : nat, a - b - a = 0.
intros. apply minus_le_O. apply minus_le_lem2.
Qed. Hint Resolve minus_minus_lem1.

Lemma minus_minus_lem2 : forall a b : nat, b <= a -> a - (a - b) = b.
simple induction b. intros. elim minus_n_O. elim minus_n_n. trivial with v62. intros.
replace (a - (a - S n)) with (S a - S (a - S n)).
rewrite <- (minus_Sn_m a (S (a - S n))). rewrite (minus_Sn_m a (S n)).
simpl in |- *. rewrite <- H. rewrite H. rewrite H. trivial with v62.
apply le_Sn_le. exact H0.
apply le_Sn_le. exact H0. apply le_Sn_le. exact H0. exact H0.
rewrite minus_Sn_m. simpl in |- *. apply minus_le_lem2. exact H0. simpl in |- *. trivial with v62.
Qed.

Lemma le_minus_minus : forall a b c : nat, c <= b -> a - b <= a - c.
simple induction a. simpl in |- *. auto with v62.
intros. generalize H0. elim c. elim minus_n_O. intro. apply minus_le_lem2.
elim b. intros. absurd (S n0 <= 0). auto with v62.
exact H2.
intros. simpl in |- *. apply H. apply le_S_n. exact H3.
Qed.