# Library RSA.MiscRsa

Require Import Arith.
Require Export Euclid.
Require Import ZArith.

Theorem lt_mult_right : x y z t : nat, x < zy < tx × y < z × t.
intros x y z t; case x; case z.
intros H'; inversion H'.
simpl in |- *; intros n H'; case t; auto with arith.
intros H'0; inversion H'0.
intros n H'; inversion H'.
intros n n0 H'; case t.
intros H'0; inversion H'0.
intros n1 H'0; apply lt_trans with (m := S n0 × S n1).
apply mult_S_lt_compat_l; auto.
rewrite (mult_comm (S n0)); rewrite (mult_comm (S n)); auto.
apply mult_S_lt_compat_l; auto.
Qed.

Theorem le_mult_right : x y : nat, 0 < yx x × y.
intros x y; case y.
intros H'; inversion H'.
intros n H'; rewrite mult_comm; simpl in |- *; auto with arith.
Qed.

Fixpoint factorial (n : nat) : nat :=
match n with
| O ⇒ 1
| S n'n × factorial n'
end.

Fixpoint power (x n : nat) {struct n} : nat :=
match n with
| O ⇒ 1
| S n'x × power x n'
end.

Lemma power_SO : x : nat, power 1 x = 1.
Proof.
simple induction x; auto.
intros; simpl in |- *; rewrite plus_comm; simpl in |- *; auto.
Qed.

Lemma power_lt_O : x n : nat, 0 < x → 0 < power x n.
simple induction n; simpl in |- *; auto with arith.
intros n0; case x; intros.
simpl in |- *; auto.
change (0 × 0 < S n1 × power (S n1) n0) in |- ×.
apply lt_mult_right; auto.
Qed.

Lemma power_le : x n : nat, 0 < nx power x n.
Proof.
intros x n; case n; simpl in |- *; auto.
intros H'; inversion H'.
intros n'; case x; intros; auto.
apply le_mult_right; auto.
apply power_lt_O; auto with arith.
Qed.

Lemma power_mult :
x a b : nat, power x a × power x b = power x (a + b).
Proof.
simple induction a; simpl in |- *; auto.
intros n H' b; rewrite mult_assoc_reverse; rewrite H'; auto.
Qed.

Lemma power_power : x a b : nat, power (power x a) b = power x (a × b).
Proof.
simple induction b; simpl in |- *; auto.
rewrite mult_comm; simpl in |- *; auto.
intros n H'; rewrite mult_comm with (m := S n); simpl in |- *;
rewrite (mult_comm n); rewrite H'; apply power_mult.
Qed.

Lemma SO_power : x : nat, power 1 x = 1.
Proof.
simple induction x; simpl in |- *; auto.
intros n H'; rewrite H'; auto.
Qed.

Lemma power_O : n : nat, 1 npower 0 n = 0.
Proof.
simple induction n.
intros; absurd (1 0); auto with arith.
intros; simpl in |- *; auto.
Qed.

Definition plus_eq := f_equal2 plus.

Definition mult_eq := f_equal2 mult.

Definition minus_eq := f_equal2 minus.

Lemma lt_minus_O_lt : n m : nat, m < n → 0 < n - m.
Proof.
intros n m H'.
apply plus_lt_reg_l with (p := m).
rewrite <- le_plus_minus; auto with arith.
rewrite plus_comm; auto.
Qed.

Lemma eq_minus : a b c : nat, c < aa - c = b - ca = b.
Proof.
intros a b c H' H'0.
rewrite (le_plus_minus c a); auto with arith.
rewrite (le_plus_minus c b); auto with arith.
apply lt_le_weak.
apply lt_O_minus_lt.
rewrite <- H'0; auto.
apply lt_minus_O_lt; auto.
Qed.

Lemma eq_minus' :
a b c : nat, c ac ba - c = b - ca = b.
Proof.
intros.
rewrite (le_plus_minus c a); auto with arith.
rewrite H1.
rewrite <- le_plus_minus; auto.
Qed.

Lemma eq_plus : a b c : nat, c + a = c + ba = b.
Proof.
intros a b c H'.
apply plus_reg_l with (p := c); auto.
Qed.

Lemma plus_eqO : x y : nat, x + y = 0 → x = 0.
Proof.
intros x; case x; simpl in |- *; auto.
intros x' y; case y; simpl in |- *; intros; discriminate.
Qed.

Lemma mult_eqO : a b : nat, a × b = 0 → a = 0 b = 0.
Proof.
intros x; case x; simpl in |- *; auto.
intros x' y; case y; simpl in |- *; auto; intros; discriminate.
Qed.

Lemma mult_SO : x y : nat, x × y = 1 → x = 1.
Proof.
intros x; case x; simpl in |- *; auto.
intros x' y; case y; simpl in |- *; auto.
rewrite mult_comm; intros; discriminate.
intros n H'; case (mult_eqO x' (S n)).
apply plus_eqO with (y := n).
intros H'0; rewrite H'0; auto.
intros; discriminate.
Qed.

Lemma mult_eq_Sn : a b : nat, 0 < ba × b = ba = 1.
Proof.
intros a b; case b; simpl in |- *; auto.
intros H; inversion H.
case a; simpl in |- *; auto.
intros; discriminate.
intros b' a' H' H'1; case (mult_eqO b' (S a')); auto.
apply plus_reg_l with (p := S a'); simpl in |- *; rewrite <- plus_n_O; auto.
intros H'0; absurd (0 < S a'); auto; rewrite H'0; auto with arith.
Qed.

Inductive is_div : natnatnatnatProp :=
is_div_def :
a b q r : nat, r < ba = q × b + ris_div a b q r.

Inductive ex_div : natnatProp :=
ex_div_def : a b q r : nat, is_div a b q rex_div a b.

Lemma div_x_nO : x y q r : nat, is_div x y q ry 0.
Proof.
intros x y q r; case y; auto.
intros H'; inversion_clear H'.
absurd (0 > r); auto with arith.
Qed.

Lemma div_x_O_r : x q r : nat, is_div 0 x q rr = 0.
Proof.
intros x q r H'; inversion_clear H'.
apply plus_eqO with (y := q × x); rewrite plus_comm; auto with arith.
Qed.

Lemma div_x_O_q : x q r : nat, is_div 0 x q rq = 0.
Proof.
intros x q r H'.
rewrite (div_x_O_r x q r) in H'; inversion H'; auto.
case (mult_eqO q x); auto.
apply plus_eqO with (y := 0); auto.
intros H'1; absurd (x > 0); auto; rewrite H'1; auto with arith.
Qed.

Lemma div_pred :
x y q : nat,
0 < xis_div x y q 0 → is_div (pred x) y (pred q) (pred y).
Proof.
intros x y q H' H'0; inversion_clear H'0.
apply is_div_def; auto with arith.
rewrite H0; auto.
rewrite <- plus_n_O; auto.
generalize H0; case q; simpl in |- *; auto.
intros H'0; absurd (0 < x); auto.
rewrite H'0; auto with arith.
intros n H'0; generalize H; case y; simpl in |- *; auto with arith.
intros H'1; absurd (0 < 0); auto with arith.
Qed.

Lemma div_SxS :
x y q r : nat,
0 < ris_div x y q ris_div (pred x) y q (pred r).
Proof.
intros x y q r H' H'1; inversion_clear H'1.
apply is_div_def; auto with arith.
generalize H; case r; simpl in |- *; auto with arith.
rewrite H0; generalize H'; case r; simpl in |- *; auto.
intros H'1; absurd (0 < 0); auto with arith.
intros r'; rewrite <- plus_n_Sm; auto.
Qed.

Lemma div_unic_r :
a b q1 q2 r1 r2 : nat,
is_div a b q1 r1is_div a b q2 r2r1 = r2.
intros a; elim a; auto.
intros b q1 q2 r1 r2 H' H'0.
apply trans_eq with (y := 0); auto.
apply div_x_O_r with (x := b) (q := q1); auto.
apply sym_eq; apply div_x_O_r with (x := b) (q := q2); auto.
intros n H' b q1 q2 r1 r2; case r1; case r2; auto.
intros n0 H'0 H'1; inversion_clear H'0; inversion_clear H'1.
cut (S n0 = (q1 - q2) × b); [ intros EqSn0 | idtac ].
generalize H1; rewrite EqSn0; case (q1 - q2); auto with arith.
intros n1 H'0; absurd (b > S n1 × b); auto; simpl in |- *; auto with arith.
rewrite mult_minus_distr_r; apply plus_minus.
rewrite (plus_n_O (q1 × b)); rewrite <- H0; auto.
intros n0 H'0 H'1; inversion_clear H'0; inversion_clear H'1.
cut (S n0 = (q2 - q1) × b); [ intros EqSn0 | idtac ].
generalize H; rewrite EqSn0; case (q2 - q1); auto with arith.
intros n1 H'0; absurd (b > S n1 × b); auto; simpl in |- *; auto with arith.
rewrite mult_minus_distr_r; apply plus_minus.
rewrite (plus_n_O (q2 × b)); rewrite <- H0; auto.
intros n0 n1 H'0 H'1; rewrite (H' b q1 q2 n1 n0); auto.
apply (div_SxS (S n) b q1 (S n1)); auto with arith.
apply (div_SxS (S n) b q2 (S n0)); auto with arith.
Qed.

Theorem simpl_mult_r : n m p : nat, 0 < nm × n = p × nm = p.
intros n m; elim m; simpl in |- *; auto.
intros p H' H'0; case (mult_eqO p n); auto.
intros H'1; absurd (0 < n); auto; rewrite H'1; auto with arith.
intros m' H' p; case p; simpl in |- *; auto.
case n; simpl in |- *; intros; try discriminate; absurd (0 < 0);
auto with arith.
intros p' H'0 H'1.
rewrite (H' p'); auto.
apply plus_reg_l with (p := n); auto.
Qed.

Lemma div_unic_q :
a b q1 q2 r1 r2 : nat,
is_div a b q1 r1is_div a b q2 r2q1 = q2.
Proof.
intros a b; case b; auto.
intros q1 q2 r1 r2 H' H'0; inversion_clear H'0; inversion_clear H'.
inversion H1; auto.
intros b' q1 q2 r1 r2 H' H'0.
rewrite (div_unic_r a (S b') q1 q2 r1 r2) in H'; auto.
inversion_clear H'0; inversion_clear H'.
apply simpl_mult_r with (n := S b'); auto with arith.
apply plus_reg_l with (p := r2).
repeat rewrite (plus_comm r2); rewrite <- H2; auto.
Qed.

Lemma quot_eq :
a b c q1 r1 q2 r2 : nat,
a = bis_div a c q1 r1is_div b c q2 r2q1 = q2.
Proof.
intros.
rewrite H in H0.
apply div_unic_q with (1 := H0) (2 := H1); auto.
Qed.

Lemma mult_div_r : x y q r : nat, is_div (x × y) y q rr = 0.
intros x y q r H'.
apply div_unic_r with (a := x × y) (b := y) (q1 := q) (q2 := x);
auto with arith.
apply is_div_def; inversion_clear H'; auto with arith.
apply le_lt_trans with (m := r); auto with arith.
Qed.

Lemma mult_div_q : x y q r : nat, is_div (x × y) y q rq = x.
Proof.
intros x y q r H'.
apply div_unic_q with (a := x × y) (b := y) (r1 := r) (r2 := 0); auto.
apply is_div_def; inversion_clear H'; auto with arith.
apply le_lt_trans with (m := r); auto with arith.
Qed.

Lemma diveucl_divex :
a b : nat,
diveucl a b q : _, ( r : _, is_div a b q r).
Proof.
intros.
elim H.
intros q r H' H'0; q; r; split; auto.
Qed.

Lemma div_ex :
a b : nat, b 0 → q : _, ( r : _, is_div a b q r).
Proof.
intros.
apply diveucl_divex.
apply eucl_dev.
generalize H; case b; auto with arith.
Qed.

Lemma eq_mult : a b c : nat, c 0 → c × a = c × ba = b.
Proof.
intros a b c; case c; auto.
intros H'; case H'; auto.
intros n H' H'0; apply simpl_mult_r with (n := S n);
repeat rewrite mult_comm with (m := S n); auto with arith.
Qed.

Lemma le_plus_le : a b c d : nat, a ba + c = b + dd c.
Proof.
intros.
cut (c = b - a + d).
intros H1; rewrite H1.
auto with arith.
apply plus_reg_l with (p := a); auto.
rewrite plus_assoc.
rewrite le_plus_minus_r; auto.
Qed.

Lemma plus_minus_assoc : a b c : nat, b aa - b + c = a + c - b.
Proof.
simple induction c.
repeat rewrite plus_comm with (m := 0); simpl in |- *; auto.
intros.
rewrite plus_comm; simpl in |- *; rewrite plus_comm.
rewrite H; auto.
rewrite <- plus_Snm_nSm.
rewrite minus_Sn_m; auto with arith.
Qed.