Require Import Arith.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Wf_nat.
Require Export MiscRsa.

Inductive divides : nat → nat → Prop :=
    dividesDef : ∀ a b q : nat, b = q × a → divides a b.

Lemma div_ref : ∀ a : nat, divides a a.
intros a; apply dividesDef with (q := 1); auto with arith.
Qed.

Lemma div_divides :
 ∀ x y : nat, (∃ q : _, is_div x y q 0) → divides y x.
Proof.
intros x y H'; elim H'; intros q E; inversion_clear E; clear H'.
apply dividesDef with (q := q); auto.
rewrite H0; auto with arith.
Qed.

Lemma divides_div :
 ∀ x y : nat, 0 < y → divides y x → ∃ q : _, is_div x y q 0.
Proof.
intros x y H'1 H'2; inversion H'2.
∃ q; auto.
apply is_div_def; auto with arith.
rewrite H; auto.
Qed.

Lemma divides_dec' :
 ∀ x y : nat,
 {(∃ q : _, is_div x y q 0)} + {¬ (∃ q : _, is_div x y q 0)}.
Proof.
intros x y; case y; auto.
right; red in |- *; intros H'; elim H'; intros q E; inversion E; clear H';
 auto.
inversion H.
intros y'; case (eucl_dev (S y') (gt_Sn_O y') x).
intros q r; case r; auto.
intros H' H'0; left; ∃ q; auto.
apply is_div_def; auto; rewrite H'0; auto with arith.
intros n H' H'0; right; red in |- *; intros H'1; elim H'1; intros q0 E;
 clear H'1.
absurd (0 = S n); auto with arith.
apply div_unic_r with (a := x) (b := S y') (q1 := q0) (q2 := q); auto.
apply is_div_def; auto with arith.
Qed.

Lemma divides_dec : ∀ x y : nat, {divides x y} + {¬ divides x y}.
intros x y; case x; case y; auto.
left; apply dividesDef with (q := 0); auto.
intros n; right; red in |- *; intros H'; inversion_clear H'.
rewrite (mult_comm q 0) in H; discriminate.
intros n; left; apply dividesDef with (q := 0); auto.
intros x' y'; case (divides_dec' (S x') (S y')); auto.
intros H'; left; apply div_divides; auto.
intros H'; right; red in |- *; intros H'0; case H'; auto.
inversion H'0.
∃ q; auto.
apply is_div_def; auto with arith.
rewrite H; auto with arith.
Qed.

Lemma all_divides_O : ∀ n : nat, divides n 0.
Proof.
intros n; apply dividesDef with (q := 0); auto.
Qed.

Lemma SO_divides_all : ∀ n : nat, divides 1 n.
Proof.
intros n; apply dividesDef with (q := n); auto with arith.
Qed.

Lemma divides_plus1 :
 ∀ a b c : nat, divides a b → divides a c → divides a (b + c).
Proof.
intros a b c H' H'0; inversion_clear H'; inversion_clear H'0.
apply dividesDef with (q := q + q0); auto.
rewrite H; rewrite H0; auto with arith.
Qed.

Lemma divides_plus2 :
 ∀ a b c : nat, divides a b → divides a (b + c) → divides a c.
Proof.
intros a b c H' H'0; inversion_clear H'; inversion_clear H'0.
apply dividesDef with (q := q0 - q).
rewrite mult_minus_distr_r.
rewrite <- H; rewrite <- H0.
rewrite minus_plus; auto.
Qed.

Theorem divides_le : ∀ a b : nat, b ≠ 0 → divides a b → a ≤ b.
intros a b; case b.
intros H'; case H'; auto.
intros n H' H'0; inversion_clear H'0.
rewrite H; generalize H; case q; simpl in |- *; auto with arith; intros;
 discriminate.
Qed.

Lemma divides_antisym : ∀ a b : nat, divides a b → divides b a → a = b.
Proof.
intros a b; case a; case b; auto.
intros b' H' H'1; inversion_clear H'.
rewrite H; auto with arith.
intros a' H' H'1; inversion_clear H'1.
rewrite H; auto with arith.
intros n n0 H' H'0; apply le_antisym; apply divides_le; auto.
Qed.

Lemma not_lt_div : ∀ a b : nat, 0 < b → b < a → ¬ divides a b.
intros a b H'1 H'2; red in |- *; intros H'3; absurd (a ≤ b); auto with arith.
apply divides_le; auto.
apply sym_not_eq; auto with arith.
Qed.

Inductive prime : nat → Prop :=
    primeDef :
      ∀ a : nat,
      a ≠ 1 → (∀ b : nat, divides b a → b ≠ 1 → a = b) → prime a.

Lemma not_prime_O : ¬ prime 0.
Proof.
red in |- *; intros H'; inversion_clear H'; auto.
absurd (0 = 2); auto with arith.
apply H0; auto.
apply all_divides_O.
Qed.

Lemma not_prime_1 : ¬ prime 1.
Proof.
red in |- *; intros H'; inversion_clear H'; auto.
Qed.
Hint Resolve div_ref all_divides_O SO_divides_all not_prime_O not_prime_1.

Lemma lt_prime : ∀ p : nat, prime p → 1 < p.
Proof.
intros p; case p.
intro; absurd (prime 0); auto.
intros n; case n.
intro; absurd (prime 1); auto.
intros; auto with arith.
Qed.

Inductive is_gcd (a b c : nat) : Prop :=
    is_gcd_intro :
      divides c a →
      divides c b →
      (∀ d : nat, divides d a → divides d b → divides d c) →
      is_gcd a b c.

Lemma is_gcd_unic :
 ∀ a b c d : nat, is_gcd a b c → is_gcd a b d → c = d.
Proof.
intros a b c d H' H'0; inversion_clear H'; inversion_clear H'0.
apply divides_antisym; auto.
Qed.

Lemma is_gcd_ref : ∀ x : nat, is_gcd x x x.
Proof.
intros x; apply is_gcd_intro; auto.
Qed.

Lemma is_gcd_sym : ∀ a b c : nat, is_gcd a b c → is_gcd b a c.
intros a b c H; inversion_clear H; intros.
apply is_gcd_intro; auto.
Qed.

Lemma is_gcd_O' : ∀ a r : nat, is_gcd a 0 r → a = r.
Proof.
intros a r H'; inversion_clear H'.
apply divides_antisym; auto.
Qed.

Lemma is_gcd_Ol : ∀ a : nat, is_gcd a 0 a.
intros a.
apply is_gcd_intro; auto.
Qed.

Lemma is_gcd_Or : ∀ a : nat, is_gcd 0 a a.
intros a.
apply is_gcd_intro; auto.
Qed.

Lemma prime_gcd : ∀ p n : nat, prime p → ¬ divides p n → is_gcd n p 1.
intros p n H' H'0.
apply is_gcd_intro; auto.
intros d H'1 H'2.
inversion_clear H'.
elim (eq_nat_dec d 1); intros H'4; auto.
rewrite H'4; auto.
elim (eq_nat_dec p d); intros H'5; auto.
case H'0; try rewrite H'5; auto.
case H'5; apply H0; auto.
Qed.

Lemma gcd_rec :
 ∀ P : nat → nat → Set,
 (∀ x : nat, P 0 x) →
 (∀ x : nat, P x 0) →
 (∀ a b : nat, P a b → P a (b + a)) →
 (∀ a b : nat, P a b → P (a + b) b) → ∀ a b : nat, P a b.
Proof.
intros P H H0 H1 H2 a; pattern a in |- *; apply lt_wf_rec.
intros a' H' b; pattern b in |- *; apply lt_wf_rec.
intros b' H'0.
case (lt_eq_lt_dec a' b'); intros Ca'b';
 [ case Ca'b'; clear Ca'b'; intros Ca'b' | idtac ].
2: rewrite Ca'b'; auto.
2: pattern b' at 1 in |- *; replace b' with (0 + b'); auto.
replace b' with (b' - a' + a'); auto with arith.
case (zerop a'); intros lta'.
rewrite lta'; auto.
apply H1; apply H'0; auto with arith.
rewrite plus_comm; auto with arith.
replace a' with (a' - b' + b'); auto with arith.
case (zerop b'); intros ltb'.
rewrite ltb'; auto.
apply H2; apply H'; auto with arith.
rewrite plus_comm; auto with arith.
Qed.

Lemma gcd_ind :
 ∀ P : nat → nat → Prop,
 (∀ x : nat, P 0 x) →
 (∀ x : nat, P x 0) →
 (∀ a b : nat, P a b → P a (b + a)) →
 (∀ a b : nat, P a b → P (a + b) b) → ∀ a b : nat, P a b.
Proof.
intros P H H0 H1 H2 a; pattern a in |- *; apply lt_wf_ind.
intros a' H' b; pattern b in |- *; apply lt_wf_ind.
intros b' H'0.
case (lt_eq_lt_dec a' b'); intros Ca'b';
 [ case Ca'b'; clear Ca'b'; intros Ca'b' | idtac ].
2: rewrite Ca'b'; auto.
2: pattern b' at 1 in |- *; replace b' with (0 + b'); auto.
replace b' with (b' - a' + a'); auto with arith.
case (zerop a'); intros lta'.
rewrite lta'; auto.
apply H1; apply H'0; auto with arith.
rewrite plus_comm; auto with arith.
replace a' with (a' - b' + b'); auto with arith.
case (zerop b'); intros ltb'.
rewrite ltb'; auto.
apply H2; apply H'; auto with arith.
rewrite plus_comm; auto with arith.
Qed.

Inductive gcd_spec : nat → nat → nat → Prop :=
  | gcd_spec_ex0 : ∀ a : nat, gcd_spec a 0 a
  | gcd_spec_ex1 : ∀ b : nat, gcd_spec 0 b b
  | gcd_spec_ex2 :
      ∀ a b c : nat, a < b → gcd_spec a (b - a) c → gcd_spec a b c
  | gcd_spec_ex3 :
      ∀ a b c : nat, b ≤ a → gcd_spec (a - b) b c → gcd_spec a b c.
Hint Resolve gcd_spec_ex0 gcd_spec_ex1.

Theorem gcd_inv_Or_aux : ∀ a b c : nat, gcd_spec a b c → b = 0 → a = c.
intros a b c H'; elim H'; auto.
intros a0 b0 c0 H'0 H'1 H'2 H'3.
apply H'2; auto.
rewrite H'3; auto.
intros a0 b0 c0 H'0 H'1 H'2 H'3.
replace a0 with (a0 - b0); auto.
rewrite H'3; auto with arith.
Qed.

Theorem gcd_inv_Or : ∀ a b : nat, gcd_spec a 0 b → a = b.
intros a b H'.
apply gcd_inv_Or_aux with (b := 0); auto.
Qed.

Theorem gcd_inv_Ol_aux : ∀ a b c : nat, gcd_spec a b c → a = 0 → b = c.
intros a b c H'; elim H'; auto.
intros a0 b0 c0 H'0 H'1 H'2 H'3.
replace b0 with (b0 - a0); auto.
rewrite H'3; auto with arith.
intros a0 b0 c0 H'0 H'1 H'2 H'3.
apply H'2; auto.
rewrite H'3; auto.
Qed.

Theorem gcd_inv_Ol : ∀ a b : nat, gcd_spec 0 a b → a = b.
intros a b H'.
apply gcd_inv_Ol_aux with (a := 0); auto.
Qed.

Definition gcd' :=
  gcd_rec (fun _ _ : nat ⇒ nat) (fun x : nat ⇒ x)
    (fun x : nat ⇒ x) (fun x y r : nat ⇒ r) (fun x y r : nat ⇒ r).

Lemma gcd_ex : ∀ a b : nat, {r : nat | gcd_spec a b r}.
intros a b; pattern b, a in |- *; apply gcd_rec; clear a b.
intros a; ∃ a; auto.
intros b; ∃ b; auto.
intros a b Rr; case Rr; intros r Hr; ∃ r.
apply gcd_spec_ex3; auto with arith.
rewrite plus_comm; rewrite minus_plus; auto; rewrite <- minus_n_n; auto.
intros a b Rr; case Rr; intros r Hr; ∃ r.
case (zerop a); intros lta.
rewrite lta; simpl in |- ×.
rewrite <- (gcd_inv_Or b r); auto.
apply gcd_spec_ex3; auto with arith.
rewrite <- minus_n_n; auto.
rewrite <- lta; auto.
apply gcd_spec_ex2; auto with arith.
pattern b at 1 in |- *; replace b with (0 + b); auto with arith.
rewrite plus_comm; rewrite minus_plus; auto; rewrite <- minus_n_n; auto.
Qed.

Definition gcd (a b : nat) := proj1_sig (gcd_ex a b).

Lemma gcd_correct : ∀ a b : nat, gcd_spec a b (gcd a b).
Proof.
intros a b; unfold gcd in |- *; case (gcd_ex a b); simpl in |- *; auto.
Qed.
Hint Resolve gcd_correct.

Lemma gcd_spec_uniq :
 ∀ a b r1 r2 : nat, gcd_spec a b r1 → gcd_spec a b r2 → r1 = r2.
intros a b r1 r2 H'; generalize r2; elim H'; clear H' a b r1 r2.
exact gcd_inv_Or.
exact gcd_inv_Ol.
intros a b c H' H'0 H'1 r2 H'2; inversion H'2; auto.
apply H'1; auto.
rewrite <- H0; simpl in |- *; rewrite H1; auto.
apply H'1; auto.
rewrite <- H; simpl in |- *; rewrite <- minus_n_O; rewrite H1; auto.
absurd (a < b); auto with arith.
intros a b c H' H'0 H'1 r2 H'2; inversion H'2; auto.
apply H'1; auto.
rewrite <- H0; simpl in |- *; rewrite H1; rewrite <- minus_n_O; auto.
apply H'1; auto.
rewrite <- H; simpl in |- *; rewrite H1; auto.
absurd (a < b); auto with arith.
Qed.

Lemma gcd_correct2 : ∀ a b r : nat, gcd_spec a b r → gcd a b = r.
Proof.
intros a b r H'.
apply gcd_spec_uniq with (a := a) (b := b); auto.
Qed.

Lemma gcd_def0l : ∀ x : nat, gcd 0 x = x.
Proof.
intros x; apply gcd_spec_uniq with (a := 0) (b := x); auto.
Qed.

Lemma gcd_def0r : ∀ x : nat, gcd x 0 = x.
Proof.
intros x; apply gcd_spec_uniq with (a := x) (b := 0); auto.
Qed.

Lemma gcd_def1 : ∀ x : nat, gcd x x = x.
Proof.
intros x; apply gcd_spec_uniq with (a := x) (b := x); auto.
apply gcd_spec_ex3; auto.
rewrite <- minus_n_n; auto.
Qed.

Lemma gcd_def2 : ∀ a b : nat, gcd a b = gcd a (b + a).
Proof.
intros a b; apply gcd_spec_uniq with (a := a) (b := b + a); auto.
case (zerop b); intros ltb.
rewrite ltb; simpl in |- *; rewrite gcd_def0r; auto.
apply gcd_spec_ex3; auto.
rewrite <- minus_n_n; auto.
apply gcd_spec_ex2; auto with arith.
replace a with (0 + a); auto with arith.
rewrite plus_comm; rewrite minus_plus.
apply gcd_correct; auto.
Qed.

Lemma gcd_def3 : ∀ a b : nat, gcd a b = gcd (a + b) b.
Proof.
intros a b; apply gcd_spec_uniq with (a := a + b) (b := b); auto.
case (zerop a); intros lta.
rewrite lta; simpl in |- *; rewrite gcd_def0l; auto.
apply gcd_spec_ex3; auto with arith.
rewrite <- minus_n_n; auto.
apply gcd_spec_ex3; auto with arith.
rewrite plus_comm; rewrite minus_plus.
apply gcd_correct; auto.
Qed.

Lemma gcd_is_gcd : ∀ a b : nat, is_gcd a b (gcd a b).
Proof.
intros; pattern a, b in |- *; apply gcd_ind; clear a b.
intros x; rewrite gcd_def0l; auto.
apply is_gcd_Or; auto.
intros x; rewrite gcd_def0r; auto.
apply is_gcd_Ol; auto.
intros a b H'; rewrite <- gcd_def2.
inversion_clear H'.
apply is_gcd_intro; auto.
apply divides_plus1; auto.
intros d H' H'0.
apply H1; auto.
apply divides_plus2 with (b := a); auto.
rewrite plus_comm; auto.
intros a b H'; rewrite <- gcd_def3.
inversion_clear H'.
apply is_gcd_intro; auto.
apply divides_plus1; auto.
intros d H' H'0.
apply H1; auto.
apply divides_plus2 with (b := b); auto.
rewrite plus_comm; auto.
Qed.

Lemma preEuclid :
 ∀ a b c m : nat,
 divides c (m × a) → divides c (m × b) → divides c (m × gcd a b).
Proof.
intros a b; pattern a, b in |- *; apply gcd_ind; clear a b.
intros x c m H' H'0; rewrite gcd_def0l; auto.
intros x c m H' H'0; rewrite gcd_def0r; auto.
intros a b H' c m H'0 H'1; rewrite <- gcd_def2.
apply H'; auto.
apply divides_plus2 with (m × a); auto.
rewrite mult_comm; pattern mult at 1 in |- *; rewrite mult_comm;
 rewrite <- mult_plus_distr_r; rewrite mult_comm.
rewrite plus_comm; simpl in |- *; assumption.
intros a b H' c m H'0 H'1; rewrite <- gcd_def3.
apply H'; auto.
apply divides_plus2 with (m × b); auto.
rewrite mult_comm; pattern mult at 1 in |- *; rewrite mult_comm;
 rewrite <- mult_plus_distr_r; rewrite mult_comm.
rewrite plus_comm; simpl in |- *; assumption.
Qed.

Theorem L_Euclides :
 ∀ x a b : nat, is_gcd x a 1 → divides x (a × b) → divides x b.
Proof.
intros x a b H' H'0; replace b with (b × gcd x a).
apply preEuclid; auto with arith.
apply dividesDef with (q := b); auto with arith.
rewrite mult_comm; auto.
rewrite (is_gcd_unic x a (gcd x a) 1); auto with arith.
apply gcd_is_gcd; auto.
Qed.

Lemma L_Euclides1 :
 ∀ p a b : nat,
 prime p → divides p (a × b) → ¬ divides p a → divides p b.
intros; apply L_Euclides with a; auto.
apply is_gcd_sym.
apply prime_gcd; auto.
Qed.

Lemma L_Euclides2 :
 ∀ p a b : nat,
 prime p → divides p (a × b) → divides p a ∨ divides p b.
intros.
elim (divides_dec p a); [ left | right ]; auto.
apply L_Euclides1 with a; auto.
Qed.

Theorem div_power_prime :
 ∀ p w n : nat, prime p → divides p (power w n) → divides p w.
intros p w n; elim n; simpl in |- *; auto.
intros H' H'0; inversion_clear H'0.
generalize H' H; case q; case p; simpl in |- *; intros; try discriminate.
absurd (prime 0); auto.
generalize H0; case n0; simpl in |- *; auto.
intros n2 H'1; absurd (1 = S (S (n2 + n1 × S (S n2)))); auto.
intros n0 H' H'0 H'1.
case (divides_dec p (power w n0)); intros H; auto.
apply L_Euclides1 with (a := power w n0); auto.
rewrite mult_comm; auto.
Qed.
Section CD.
Variable n : nat.

Inductive congruent : nat → nat → Prop :=
    congruentDef :
      ∀ a b u v : nat, a + u × n = b + v × n → congruent a b.

Lemma cong_ref : ∀ a : nat, congruent a a.
Proof.
intros a.
apply congruentDef with (u := 1) (v := 1); auto.
Qed.

Lemma cong_sym : ∀ a b : nat, congruent a b → congruent b a.
Proof.
intros a b H; elim H.
intros a0 b0 c d H'.
apply congruentDef with (u := d) (v := c); auto.
Qed.

Lemma cong_trans :
 ∀ a b c : nat, congruent a b → congruent b c → congruent a c.
Proof.
intros a b c H' H'0; inversion_clear H'; inversion_clear H'0.
apply congruentDef with (u := u + u0) (v := v + v0); auto.
repeat rewrite mult_plus_distr_r; repeat rewrite plus_assoc; rewrite H.
repeat rewrite plus_comm with (m := v × n); repeat rewrite plus_assoc_reverse;
 rewrite H0; auto.
Qed.

Lemma cong_mult_O : ∀ a b : nat, congruent a 0 → congruent (a × b) 0.
Proof.
intros a b H'; inversion_clear H'.
apply congruentDef with (u := u × b) (v := v × b).
repeat rewrite mult_comm with (m := b); repeat rewrite mult_assoc_reverse;
 repeat rewrite (mult_comm b).
rewrite <- mult_plus_distr_r; rewrite H; rewrite mult_plus_distr_r;
 simpl in |- *; auto.
Qed.

Lemma cong_plus :
 ∀ a b c d : nat,
 congruent a b → congruent c d → congruent (a + c) (b + d).
Proof.
intros a b c d H' H'0; inversion_clear H'; inversion_clear H'0.
apply congruentDef with (u := u0 + u) (v := v0 + v).
repeat rewrite mult_plus_distr_r; repeat rewrite plus_assoc_reverse.
rewrite (plus_assoc c); rewrite (plus_assoc d); rewrite H0.
rewrite (plus_comm a); rewrite (plus_comm b);
 repeat rewrite plus_assoc_reverse; rewrite plus_comm with (m := a);
 rewrite plus_comm with (m := b); rewrite H; auto.
Qed.

Lemma cong_add :
 ∀ a b c : nat, congruent a b → congruent (a + c) (b + c).
Proof.
intros a b c H; inversion_clear H.
apply congruentDef with (u := u) (v := v); auto.
repeat rewrite plus_comm with (m := c); repeat rewrite plus_assoc_reverse;
 rewrite H0; auto.
Qed.

Lemma cong_times :
 ∀ a b c : nat, congruent a b → congruent (a × c) (b × c).
intros a b c H; inversion_clear H.
apply congruentDef with (u := u × c) (v := v × c); auto.
repeat rewrite mult_comm with (m := c); repeat rewrite mult_assoc_reverse;
 repeat rewrite (mult_comm c).
repeat rewrite <- mult_plus_distr_r.
rewrite H0; auto.
Qed.

Lemma cong_mult :
 ∀ a b c d : nat,
 congruent a b → congruent c d → congruent (a × c) (b × d).
intros a b c d H' H'0; inversion_clear H'; inversion_clear H'0.
apply
 congruentDef
  with (u := u0 × a + u × u0 × n + u × c) (v := v0 × b + v × v0 × n + v × d).
repeat rewrite mult_plus_distr_r.
repeat rewrite plus_assoc.
rewrite (mult_comm u0); rewrite (mult_comm v0).
repeat rewrite mult_assoc_reverse.
repeat rewrite (mult_comm a); repeat rewrite (mult_comm b).
repeat rewrite <- mult_plus_distr_r.
repeat rewrite mult_assoc.
repeat rewrite mult_comm with (m := n).
rewrite (mult_assoc n u); rewrite (mult_assoc n v).
repeat rewrite mult_assoc.
repeat rewrite (mult_assoc_reverse n n).
rewrite mult_comm with (m := n × u); rewrite mult_comm with (m := n × v).
repeat rewrite mult_assoc_reverse with (m := n).
repeat rewrite (mult_comm (n × u)); repeat rewrite (mult_comm (n × v)).
repeat rewrite plus_assoc_reverse; repeat rewrite <- mult_plus_distr_r.
rewrite plus_comm with (m := c); rewrite plus_comm with (m := d).
repeat rewrite (mult_comm (c + n × u0));
 repeat rewrite (mult_comm (d + n × v0)).
repeat rewrite (mult_comm (c + n × u0));
 repeat rewrite (mult_comm (d + n × v0)).
repeat rewrite <- mult_plus_distr_r.
repeat rewrite (mult_comm n); rewrite H; auto.
Qed.

Lemma cong_pow :
 ∀ a b c : nat, congruent a b → congruent (power a c) (power b c).
intros a b c; elim c; simpl in |- *; auto.
intros H'; apply cong_ref.
intros n0 H' H'0.
apply cong_mult; auto.
Qed.

Theorem congruent' :
 ∀ a b : nat, b ≤ a → congruent a b → ∃ k : nat, a = k × n + b.
intros a b H' H'0; inversion_clear H'0.
∃ (v - u).
rewrite mult_minus_distr_r; auto.
rewrite plus_minus_assoc.
rewrite plus_comm; rewrite <- H; rewrite plus_comm; auto with arith.
apply le_plus_le with (a := b) (b := a); auto.
Qed.

Lemma cong1_le : ∀ x : nat, 1 < n → congruent x 1 → 1 ≤ x.
Proof.
intros x; case x; auto with arith.
intros H' H'0; inversion_clear H'0.
absurd (n = 1).
red in |- *; intros H'0; absurd (1 < n); auto; rewrite H'0; auto with arith.
apply mult_SO with (y := u - v); auto.
rewrite mult_comm.
rewrite mult_minus_distr_r; auto.
simpl in H; rewrite H.
rewrite <- minus_Sn_m; auto with arith.
Qed.

Lemma divides_cong : ∀ x : nat, divides n x → congruent 0 x.
Proof.
intros x H; inversion_clear H.
apply congruentDef with (u := q) (v := 0); simpl in |- *; rewrite H0;
 auto with arith.
Qed.

Theorem cong_divides :
 ∀ a b : nat, b ≤ a → congruent a b → divides n (a - b).
Proof.
intros a b H H0; elim (congruent' _ _ H H0).
intros x H1; ∃ x.
apply plus_reg_l with b.
rewrite le_plus_minus_r; auto.
rewrite plus_comm; rewrite <- H1; auto.
Qed.
End CD.