Current state

From Coq Require Import Arith.
From Coq Require Import Wf_nat.
From Coq Require Import ZArith.
From Coq Require Import Peano_dec.
From Coq Require Import ZArith_dec.

From Coqprime  Require Import NatAux ZCAux ZCmisc ZSum Pmod Ppow.

(** * Compatibility lemmas (provisional) *)

(** more general than [NatAux] lemma *)

Definition CoPrime (a b : nat) := (* done *)
   Zis_gcd (Z.of_nat a) (Z.of_nat b) 1%Z.

Lemma coPrimeSym (* done *) : forall a b : nat, CoPrime a b -> CoPrime b a.
Proof. intros. now apply Zis_gcd_sym. Qed.

Definition LinComb (c x y: Z) := exists a b: Z, c = x * a + y * b.

Lemma gcd_lincomb_nat:
  forall (x y d : nat),
  (x > 0)%nat ->
  Zis_gcd (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) ->
  LinComb (Z_of_nat d) (Z_of_nat x) (Z_of_nat y).
Proof.
Admitted.

Lemma coPrimeMult : (* done *)
  forall a b c : nat, CoPrime a b -> divide a (b * c) -> divide a c.
Proof.
  intros ? ? ? H H0; unfold CoPrime in H.
  induction a as [| a _].
  - (* a = 0 *)
    induction H0 as (x, H0).
    cbn in H0. rewrite Nat.eq_mul_0 in H0. (* b = O \/ c = O *)
    destruct H0 as [H1 | H1].
    + rewrite H1 in H. simpl in H.
      inversion H. clear H H0 H1 H2.
      assert (2 | 0). { exists 0. auto. }
      destruct (H3 _ H H). nia.
    + rewrite H1. exists 0%nat. auto.
  - assert (H1: (S a > 0)%nat) by apply gt_Sn_O.
    destruct (gcd_lincomb_nat _ _ 1 H1 H) as [x [x0 H2]].
    destruct H0 as [x1 H0].
    assert (1 * Z.of_nat c = Z_of_nat (S a) * (x * Z.of_nat c + Z.of_nat x1 * x0)).
    { rewrite (Z.mul_comm (Z.of_nat (S a))).
      rewrite  Z.mul_add_distr_r.
      rewrite (Z.mul_comm (x * Z.of_nat c)).
      rewrite (Z.mul_comm (Z.of_nat x1 * x0)).
      repeat rewrite Z.mul_assoc.
      rewrite <- Znat.inj_mult.
      rewrite <- H0.
      rewrite Znat.inj_mult.
      rewrite (Z.mul_comm (Z.of_nat b)).
      rewrite <- (Z.mul_assoc (Z.of_nat c)).
      rewrite (Z.mul_comm (Z.of_nat c)).
      rewrite <- Z.mul_add_distr_r.
      now rewrite <- H2. }
    rewrite Zmult_1_l in H3.
    assert (Z.divide (Z.of_nat (S a)) (Z.of_nat c)).
    { exists (x * Z.of_nat c + Z.of_nat x1 * x0).
      now rewrite Z.mul_comm at 1. }
    clear H2 H3 x x0.
    rewrite <- (Znat.Zabs2Nat.id (S a)).
    rewrite <- (Znat.Zabs2Nat.id c).
    repeat rewrite Zabs2Nat.id. destruct H4. exists (Z.to_nat x). lia.
Qed.

Lemma coPrimeMult2 : (* done *)
  forall a b c : nat,
    CoPrime a b -> divide a c -> divide b c -> divide (a * b) c.
Proof.
  intros a b c H H0 [x H1].
  assert (divide a x).
  { eapply coPrimeMult with (1:= H); now rewrite <- H1. }
  destruct H2 as [x0 H2]; exists x0; subst; ring.
Qed.

Lemma ltgt1 (* done *): forall a b : nat, (a < b -> b > 0)%nat. (* done *)
Proof. lia. Qed.

Lemma minus1 (* done *) : forall a b c : Z, (a - c)%Z = (b - c)%Z -> a = b.
Proof. lia. Qed.

Lemma chRem2 : (* done *)
  forall b1 r1 b2 r2 q : Z,
    (0 <= r1)%Z ->
    (0 <= r2)%Z ->
    (r1 < q)%Z -> (r2 < q)%Z -> (b1 * q + r1)%Z = (b2 * q + r2)%Z ->
    r1 = r2.
Proof.
  intros * H H0 H1 H2 H3.
  assert (H4: ((b1 - b2) * q)%Z = (r2 - r1)%Z) by
    (rewrite  Z.mul_sub_distr_r; lia).
  induction (Zle_or_lt 0 (b1 - b2)) as [H5 | H5].
  induction (Zle_lt_or_eq _ _ H5) as [H6 | H6].
  assert (H7: (1 <= b1 - b2)%Z).
  { replace 1%Z with (Z.succ 0).
    apply Zlt_le_succ.
    assumption.
    auto.
  }
  assert (H8:(q <= r2 - r1)%Z).
  { replace q with (1 * q)%Z.
    rewrite <- H4.
    apply Zmult_le_compat_r.
    assumption.
    eapply Z.le_trans.
    apply H.
    apply Zlt_le_weak.
    assumption.
    apply Zmult_1_l.
  }
  set (A1 := Zplus_lt_le_compat r2 q (- r1) 0 H2) in *.
  assert (H9:(r2 - r1 < q)%Z).
  { replace q with (q + 0)%Z.
    unfold Zminus in |- *.
    apply A1.
    eapply (fun a b : Z => Zplus_le_reg_l a b r1).
    rewrite Zplus_opp_r.
    rewrite <- Zplus_0_r_reverse.
    assumption.
    rewrite <- Zplus_0_r_reverse.
    reflexivity.
  }
  elim (Zle_not_lt q (r2 - r1)).
  assumption.
  assumption.
  rewrite <- H6 in H4.
  rewrite Z.mul_comm in H4.
  rewrite <- Zmult_0_r_reverse in H4.
  rewrite <- (Zplus_opp_r r2) in H4.
  unfold Zminus in H4.
  apply Z.opp_inj.
  symmetry  in |- *.
  eapply Zplus_reg_l.
  apply H4.
  assert (H6:(1 <= b2 - b1)%Z).
  { replace 1%Z with (Z.succ 0).
    apply Zlt_le_succ.
    apply (Zplus_lt_reg_l 0 (b2 - b1) b1).
    rewrite Zplus_minus.
    rewrite <- Zplus_0_r_reverse.
    apply (Zplus_lt_reg_l b1 b2 (- b2)).
    rewrite Zplus_opp_l.
    rewrite Zplus_comm.
    unfold Zminus in H5.
    assumption.
    auto.
  }
  assert (H7: ((b2 - b1) * q)%Z = (r1 - r2)%Z) by
    ( rewrite Z.mul_sub_distr_r ; lia ).
  assert (H8:(q <= r1 - r2)%Z).
  { replace q with (1 * q)%Z.
    rewrite <- H7.
    apply Zmult_le_compat_r.
    assumption.
    eapply Z.le_trans.
    apply H.
    apply Zlt_le_weak.
    assumption.
    apply Zmult_1_l.
  }
  set (A1 := Zplus_lt_le_compat r1 q (- r2) 0 H1) in *.
  assert (H9:(r1 - r2 < q)%Z).
  { replace q with (q + 0)%Z.
    unfold Zminus in |- *.
    apply A1.
    eapply (fun a b : Z => Zplus_le_reg_l a b r2).
    rewrite Zplus_opp_r.
    rewrite <- Zplus_0_r_reverse.
    assumption.
    rewrite <- Zplus_0_r_reverse.
    reflexivity.
  }
  elim (Zle_not_lt q (r1 - r2)).
  assumption.
  assumption.
Qed.



Open Scope nat_scope.

Lemma uniqueRem : (* done *)
 forall r1 r2 b : nat,
 b > 0 ->
 forall a : nat,
 (exists q : nat, a = q * b + r1 /\ b > r1) ->
 (exists q : nat, a = q * b + r2 /\ b > r2) -> r1 = r2.
Proof.
  intros ? ? ? H a [x [H0 H2]] [x0 [H1 H3]].
  assert (x = x0). { nia. } nia.
Qed.

Lemma modulo :
 forall b : nat,  b > 0 ->
 forall a : nat, {p : nat * nat | a = fst p * b + snd p /\ b > snd p}.
Proof.
  intros b H a; apply (gt_wf_rec a).
  intros n H0 .
  destruct (le_lt_dec b n) as [Hle | Hlt].
  - assert (n > n - b).
    { unfold gt in |- *; apply lt_minus; assumption. }
    destruct (H0 _ H1) as [[a1 b0] p].
    simpl in p;  exists (S a1, b0); simpl in |- *.
    destruct p as (H2, H3).
    split.
    + rewrite <- Nat.add_assoc, <- H2.
      now apply le_plus_minus.
    + assumption.
  -  exists (0, n); simpl in |- *; now split.
Qed.


Lemma chRem1 : (* done *)
 forall b : nat,  b > 0 -> forall a : Z,
     {p : Z * nat | snd p < b /\
                      Z.of_nat (snd p) = (fst p * Z.of_nat b + a)%Z}.
Proof.
  intros b H a.
  assert
    (H0: forall a' : Z,
        (a' >= 0)%Z ->
        {p : Z * nat | snd p < b /\
                         Z.of_nat (snd p) =
                           (fst p * Z.of_nat b + a')%Z}).
  { intros a' H0; set (A := Z.to_nat a') in *.
    induction (modulo b H A) as [x p].
    destruct x as (a0, b0).
    exists ((- Z.of_nat a0)%Z, b0).
    destruct p as (H1, H2).
    split.
    - apply H2.
    - rewrite <- (Z2Nat.id a').
      + simpl fst ; simpl snd.
        rewrite Zopp_mult_distr_l_reverse.
        rewrite Z.add_comm.
        fold (Z.of_nat (Z.to_nat a') - Z.of_nat a0 * Z.of_nat b)%Z
          in |- *.
        apply Zplus_minus_eq.
        rewrite <- Znat.inj_mult.
        rewrite <- Znat.inj_plus.
        apply Znat.inj_eq.
        apply H1.
      + auto.
        now rewrite <- Z.ge_le_iff.
  }
  destruct (Z_ge_lt_dec a 0).
  + apply H0; assumption.
  + assert (a + Z.of_nat b * - a >= 0)%Z.
    induction b as [| b Hrecb].
    * elim (lt_irrefl _ H).
    * rewrite Znat.inj_S.
      rewrite Z.mul_comm.
      rewrite <- Zmult_succ_r_reverse.
      fold (- a * Z.of_nat b - a)%Z in |- *.
      rewrite Zplus_minus.
      replace 0%Z with (0 * Z.of_nat b)%Z.
      apply Zmult_ge_compat_r.
      rewrite (Zminus_diag_reverse a).
      rewrite <- (Zplus_0_l (- a)).
      unfold Zminus in |- *.
      apply Z.le_ge.
      apply Zplus_le_compat_r.
      apply Zlt_le_weak.
      assumption.
      replace 0%Z with (Z.of_nat 0).
      apply Znat.inj_ge.
      unfold ge in |- *.
      apply le_O_n.
      auto.
      auto.
    * induction (H0 _ H1) as [x [H2 H3]].
      induction x as (a0, b1).
      exists ((a0 - a)%Z, b1).
      split.
      -- simpl in |- *; apply H2.
      -- cbv beta iota zeta delta [fst snd] in |- *.
         cbv beta iota zeta delta [fst snd] in H3.
         rewrite H3.
         rewrite (Zplus_comm a).
         rewrite Zplus_assoc.
         apply Zplus_eq_compat.
         rewrite Zmult_minus_distr_r.
         unfold Zminus in |- *.
         apply Zplus_eq_compat.
         reflexivity.
         rewrite Z.mul_comm.
         apply Zopp_mult_distr_l_reverse.
         reflexivity.
Qed.

Lemma euclid_gcd1 :
 forall (d : nat) (x y q r : Z), Zis_gcd x y (Z.of_nat d) -> x = (q * y + r)%Z -> Zis_gcd r y (Z.of_nat d).
Proof.
  intros. rewrite H0 in H. clear H0 x.
  replace (q * y + r)%Z with (r - (- q) * y)%Z in H by lia.
  apply Zis_gcd_sym in H. apply Zis_gcd_for_euclid in H. auto.
Qed.

Lemma euclid_gcd :
 forall (d1 d2 : nat) (x y q r : Z),
 x = (q * y + r)%Z -> Zis_gcd x y (Z.of_nat d1) -> Zis_gcd r y (Z.of_nat d2) -> d1 = d2.
Proof.
   intros. pose proof (euclid_gcd1 d1 x y q r H0 H).
   pose proof (Zis_gcd_unique r y _ _ H2 H1). lia.
Qed.

Lemma gcd_lincomb_nat_dec :
 forall x y d : nat,
 x > 0 ->
 Zis_gcd (Z.of_nat x) (Z.of_nat y) (Z.of_nat d) ->
 {a : Z * Z |
   Z.of_nat d = (Z.of_nat x * fst a + Z.of_nat y * snd a)%Z}.
Proof.
   intro x; apply (lt_wf_rec x); intros X IH. intros y d H H0.
   elim (modulo X H y).
   intro z; elim z.
   intros q r; clear z; simpl in |- *.
   case r.
   (* case r = 0 *)
   - intros; induction p as (H1, H2).
     rewrite <- plus_n_O in H1.
     exists (1%Z, 0%Z).
     simpl fst; simpl snd.
     rewrite <- Zmult_0_r_reverse; rewrite <- Zplus_0_r_reverse.
     rewrite Z.mul_comm. rewrite Zmult_1_l.
     apply Znat.inj_eq.
     apply (euclid_gcd d X (Z.of_nat y) (Z.of_nat X) (Z.of_nat q) 0).
     rewrite <- Zplus_0_r_reverse; rewrite <- Znat.inj_mult;
       apply Znat.inj_eq; assumption.
     apply Zis_gcd_sym; assumption.
     constructor.
     + exists 0%Z. auto.
     + exists 1%Z. lia.
     + auto.
   - (* case r > 0 *)
   intros r1 [H1 H2].
   elim (IH (S r1) H2 X d).
   + intro z; elim z.
     intros delta gamma; clear z.
     simpl fst; simpl snd.
   intros p.
   exists ((gamma - Z.of_nat q * delta)%Z, delta).
   simpl fst; simpl snd.
   rewrite p, H1.
   unfold Zminus in |- *; rewrite Zmult_plus_distr_r.
   rewrite Znat.inj_plus; rewrite Zmult_plus_distr_l.
   rewrite Znat.inj_mult; rewrite <- Zopp_mult_distr_l_reverse.
   rewrite (Z.mul_assoc (Z.of_nat X)).
   rewrite (Z.mul_comm (Z.of_nat X) (- Z.of_nat q)).
   rewrite Zopp_mult_distr_l_reverse.
   rewrite Zopp_mult_distr_l_reverse.
   rewrite <- (Z.add_assoc (Z.of_nat X * gamma)).
   rewrite <- Znat.inj_mult.
   rewrite (Z.add_assoc (- (Z.of_nat (q * X) * delta))).
   rewrite Zplus_opp_l. simpl in |- *. apply Z.add_comm.
   + auto with arith.
   + apply (euclid_gcd1 d (Z.of_nat y) (Z.of_nat X) (Z.of_nat q) (Z.of_nat (S r1))).
     * apply Zis_gcd_sym; assumption.
     * rewrite <- Znat.inj_mult; rewrite <- Znat.inj_plus;
          apply Znat.inj_eq; assumption.
Qed.

Lemma chineseRemainderTheoremHelp :
  forall x1 x2 : nat,
    CoPrime x1 x2 ->
    forall (a b : nat) (pa : a < x1) (pb : b < x2),
      a <= b ->
      {y : nat |
        y < x1 * x2 /\
          a = snd (proj1_sig (modulo x1 (ltgt1 _ _ pa) y)) /\
          b = snd (proj1_sig (modulo x2 (ltgt1 _ _ pb) y))}.
Proof.
  intros ? ? H a b pa pb H0. unfold CoPrime in H.
  replace 1%Z with (Z.of_nat 1) in H by auto.
  destruct (gcd_lincomb_nat_dec _ _ _ (ltgt1 _ _ pa) H)
    as [(a0,b0) p].
  set (A := Z.of_nat a) in *.
  set (B := Z.of_nat b) in *.
  set (X1 := Z.of_nat x1) in *.
  set (X2 := Z.of_nat x2) in *.
  set (y := (a0 * (B - A))%Z) in *.
  set (z := (b0 * (A - B))%Z) in *.
  set (d := (A + X1 * y)%Z) in *.
  assert (d = (B + X2 * z)%Z).
  unfold d in |- *; simpl in p.
  apply minus1 with (X2 * z)%Z.
  rewrite (Z.add_comm B).
  rewrite Zminus_plus.
  unfold z in |- *.
  replace (A - B)%Z with (- (B - A))%Z.
  unfold Zminus in |- *.
  rewrite (Z.mul_comm b0).
  rewrite Zopp_mult_distr_l_reverse.
  rewrite (Z.mul_comm X2).
  rewrite Zopp_mult_distr_l_reverse.
  rewrite Z.opp_involutive.
  unfold y in |- *.
  rewrite <- (Z.mul_assoc (B + - A)).
  rewrite (Z.mul_comm (B + - A)).
  rewrite (Z.mul_assoc X1).
  rewrite (Z.mul_comm b0).
  rewrite <- Z.add_assoc.
  rewrite <- Zmult_plus_distr_l.
  rewrite <- p.
  rewrite Z.mul_1_l.
  fold (B - A)%Z in |- *.
  apply Zplus_minus.
  unfold Zminus in |- *.
  rewrite Zopp_plus_distr.
  rewrite Z.add_comm.
  rewrite Z.opp_involutive.
  reflexivity.
  assert (H2: x1 * x2 > 0).
  replace 0 with (0 * x2).
  unfold gt in |- *.
  rewrite Nat.mul_comm.
  rewrite (Nat.mul_comm x1).
  induction x2 as [| x2 Hrecx2].
  elim (lt_n_O _ pb).
  apply mult_S_lt_compat_l.
  fold (x1 > 0) in |- *.
  eapply ltgt1.
  apply pa.
  auto.
  destruct (chRem1 _ H2 d) as [(a1, b1) [H3 H4]].
  exists b1; split.
  apply H3.
  cbv beta iota zeta delta [snd fst] in H4, p.
  split.
  induction (modulo x1 (ltgt1 a x1 pa) b1).
  induction x as (a2, b2).
  simpl in |- *.
  induction p0 as (H5, H6).
  cbv beta iota zeta delta [snd fst] in H5.
  rewrite H5 in H4.
  unfold d in H4.
  unfold A, X1 in H4.
  assert (Z.of_nat a = Z.of_nat b2).
  { eapply chRem2; try lia.
    + apply Znat.inj_lt.
      apply pa.
    + apply Znat.inj_lt.
      apply H6.
    + rewrite Znat.inj_plus in H4.
      repeat rewrite Znat.inj_mult in H4.
      symmetry  in |- *.
      rewrite (Z.add_comm (Z.of_nat a)) in H4.
      rewrite Z.add_assoc in H4.
      rewrite Z.mul_assoc in H4.
      rewrite (Z.mul_comm a1) in H4.
      rewrite <- (Z.mul_assoc (Z.of_nat x1)) in H4.
      rewrite <- Zmult_plus_distr_r in H4.
      rewrite (Z.mul_comm (Z.of_nat x1)) in H4.
      apply H4. }
  lia.
  induction (modulo x2 (ltgt1 b x2 pb) b1).
  simpl in |- *.
  induction x as (a2, b2).
  cbv beta iota zeta delta [snd fst] in p0.
  induction p0 as (H5, H6).
  rewrite H5 in H4.
  rewrite H1 in H4.
  unfold B, X2 in H4.
  simpl. assert (Z.of_nat b = Z.of_nat b2).
  { eapply chRem2; try lia.
    + apply Znat.inj_lt.
      apply pb.
    + apply Znat.inj_lt.
      apply H6.
    + rewrite Znat.inj_plus in H4.
      repeat rewrite Znat.inj_mult in H4.
      symmetry  in |- *.
      rewrite (Z.add_comm (Z.of_nat b)) in H4.
      rewrite Z.mul_assoc in H4.
      rewrite Z.add_assoc in H4.
      rewrite (Z.mul_comm a1) in H4.
      rewrite (Z.mul_comm (Z.of_nat x2)) in H4.
      rewrite <- Zmult_plus_distr_l in H4.
      apply H4. }
  lia.
Qed.

Lemma chineseRemainderTheorem :
 forall x1 x2 : nat,
 CoPrime x1 x2 ->
 forall (a b : nat) (pa : a < x1) (pb : b < x2),
 {y : nat |
 y < x1 * x2 /\
 a = snd (proj1_sig (modulo x1 (ltgt1 _ _ pa) y)) /\
 b = snd (proj1_sig (modulo x2 (ltgt1 _ _ pb) y))}.
Proof.
  intros ? ? H a b pa pb.
  destruct (le_lt_dec a b).
  - apply chineseRemainderTheoremHelp; assumption.
  - assert (H0: b <= a) by (now apply lt_le_weak).
    assert (H1: CoPrime x2 x1) by (now apply coPrimeSym).
    induction (chineseRemainderTheoremHelp _ _ H1 b a pb pa H0)
                as [x [H2 [H3 H4]]].
    exists x.
    split.
    + now rewrite Nat.mul_comm.
    + split; assumption.
Qed.

Fixpoint prod (n:nat) (x: nat -> nat) :=
  match n with
    O => 1%nat
  | S p => x p * prod p x
  end.

Definition factorial (n : nat) : nat := prod n S.

Lemma coPrime1 : forall a : nat, CoPrime 1 a.
Proof.
  split.
  - simpl. exists 1%Z. auto.
  - exists (Z.of_nat a); lia.
  - intros e [H H0] [H1 H2].
    simpl in H0. symmetry in H0.
    assert (H >= 0 \/ H <= 0)%Z by lia. destruct H3.
    + pose proof (Zmult_one _ _ H3 H0). subst. exists 1%Z. lia.
    + assert (- H >= 0)%Z by lia.
      replace (H * e)%Z with ((- H) * (- e))%Z in H0 by lia.
      pose proof (Zmult_one _ _ H4 H0). rewrite H5 in H0.
      exists (-1)%Z. lia.
Qed.

Lemma coPrimeMult3 (a b c: nat):
  a > 0 -> b > 0 -> c > 0 ->
  CoPrime a c -> CoPrime b c -> CoPrime (a * b) c.
Proof.
  intros H H0 H1 H2 H3;
    assert (H4: LinComb
                  (Z.of_nat 1) (Z.of_nat a) (Z.of_nat c)).
  { apply gcd_lincomb_nat.
    assumption.
    apply H2.
  }
  assert (H5: LinComb
               (Z.of_nat 1) (Z.of_nat b) (Z.of_nat c)).
  { apply gcd_lincomb_nat.
    assumption.
    apply H3.
  }
  destruct  H4 as [x [x0 H4]].
  destruct  H5 as [x1 [x2 H5]].
  split.
  - exists (Z.of_nat (a * b)). lia.
  - exists (Z.of_nat c). lia.
  - intros e [H6 H7].
    set (A := Z.of_nat a) in *.
    set (B := Z.of_nat b) in *.
    set (C := Z.of_nat c) in *.
    assert (H8:
             (1%Z =
                (A * B * (x * x1) +
                   C * (x0 * B * x1 + x2 * A * x + x0 * x2 * C))%Z)).
    {
      change  1%Z with (Z.of_nat 1 * Z.of_nat 1)%Z.
      rewrite H4 at 1.
      rewrite H5.
      ring; reflexivity.
    }
    intros. destruct H9. rewrite H8.
    apply Z.divide_add_r.
    + exists (H6 * x * x1)%Z. assert (A * B = Z.of_nat (a * b))%Z by lia.
      rewrite H10. rewrite H7. lia.
    + apply Z.divide_mul_l. exists x3. auto.
Qed.



Lemma prodBig1 :
 forall (n : nat) (x : nat -> nat),
 (forall z : nat, z < n -> x z > 0) -> prod n x > 0.
Proof.
  induction n as [| n Hrecn].
  - intros x H; simpl in |- *; apply gt_Sn_n.
  - intros x H; simpl in |- *; apply Nat.mul_pos_pos.
    + apply H; apply lt_n_Sn.
    + apply Hrecn; intros; now apply H, lt_S.
Qed.

Lemma sameProd :
 forall (n : nat) (x1 x2 : nat -> nat),
 (forall z : nat, z < n -> x1 z = x2 z) -> prod n x1 = prod n x2.
Proof.
induction n as [| n Hrecn].
- intros; reflexivity.
- intros x1 x2 H; simpl in |- *; replace (x1 n) with (x2 n).
  + f_equal; auto.
  + rewrite (H n); auto.
Qed.

Lemma coPrimeProd :
 forall (n : nat) (x : nat -> nat),
 (forall z1 z2 : nat,
  z1 < S n -> z2 < S n -> z1 <> z2 -> CoPrime (x z1) (x z2)) ->
 (forall z : nat, z < S n -> x z > 0) -> CoPrime (prod n x) (x n).
Proof.
  induction n as [| n Hrecn].
  - intros; simpl in |- *; apply coPrime1.
  - intros x H H0.
    assert
      (H1: forall z1 z2 : nat,
          z1 < S n -> z2 < S n -> z1 <> z2 -> CoPrime (x z1) (x z2)).
    { intros;apply H.
      1,2:  now apply Nat.lt_lt_succ_r.
      - assumption.
    }
    simpl in |- *; apply coPrimeMult3.
  + apply H0.
    apply Nat.lt_lt_succ_r.
    apply lt_n_Sn.
  + apply prodBig1.
    intros; apply H0.
    do 2 apply Nat.lt_lt_succ_r.
    assumption.
  + apply H0.
    apply lt_n_Sn.
  + apply H.
    apply Nat.lt_lt_succ_r.
    apply lt_n_Sn.
    apply lt_n_Sn.
    auto.
  + set
      (A1 :=
         fun a : nat =>
           match eq_nat_dec a n with
           | left _ => x (S n)
           | right _ => x a
           end) in *.
    assert (H2: CoPrime (prod n A1) (A1 n)).
    { apply Hrecn.
      intros.
      unfold A1 in |- *.
      induction (eq_nat_dec z1 n).
      + induction (eq_nat_dec z2 n).
        * elim H4.
          rewrite a0.
          assumption.
        * apply H.
          apply lt_n_Sn.
          apply Nat.lt_lt_succ_r.
          assumption.
          unfold not in |- *; intros.
          rewrite H5 in H3.
          elim (lt_irrefl _ H3).
      + induction (eq_nat_dec z2 n).
        * apply H.
          apply Nat.lt_lt_succ_r.
          assumption.
          apply lt_n_Sn.
          unfold not in |- *; intros.
          rewrite H5 in H2.
          elim (lt_irrefl _ H2).
        * apply H.
          apply Nat.lt_lt_succ_r.
          assumption.
          apply Nat.lt_lt_succ_r.
          assumption.
          assumption.
      + intros.
        unfold A1 in |- *.
        induction (eq_nat_dec z n).
        * apply H0.
          apply lt_n_Sn.
        * apply H0.
          apply Nat.lt_lt_succ_r.
          assumption.
    }
    auto.
    replace (x (S n)) with (A1 n).
    replace (prod n x) with (prod n A1).
    assumption.
    apply sameProd.
    intros.
    unfold A1 in |- *.
    induction (eq_nat_dec z n).
   * rewrite a in H3.
     elim (lt_irrefl _ H3).
   * reflexivity.
   * unfold A1 in |- *.
     induction (eq_nat_dec n n).
     -- reflexivity.
     -- elim b; reflexivity.
Qed.

Lemma divProd :
 forall (n : nat) (x : nat -> nat) (i : nat),
 i < n -> divide (x i) (prod n x).
Proof.
  induction n as [| n Hrecn].
  - intros x i H; destruct (lt_n_O _ H).
  - intros x i H; destruct (le_lt_or_eq i n).
     + now apply lt_n_Sm_le.
     + simpl in |- *.
      rewrite Nat.mul_comm.
      destruct (Hrecn x i H0).
      rewrite H1. exists (x0 * x n). lia.
    + subst. simpl. exists (prod n x). auto.
Qed.

Lemma chRem :
 forall (n : nat) (x : nat -> nat),
 (forall z1 z2 : nat, z1 < n -> z2 < n -> z1 <> z2 -> CoPrime (x z1) (x z2)) ->
 forall (y : nat -> nat) (py : forall z : nat, z < n -> y z < x z),
 {a : nat |
 a < prod n x /\
 (forall (z : nat) (pz : z < n),
  y z = snd (proj1_sig (modulo (x z) (ltgt1 _ _ (py z pz)) a)))}.
Proof.
  intro.
  induction n as [| n Hrecn].
  - intros; exists 0.
    split.
    + simpl in |- *.
      apply lt_O_Sn.
    + intros.
      elim (lt_n_O _ pz).
  - intros.
    assert
      (H0: forall z1 z2 : nat,
          z1 < n -> z2 < n -> z1 <> z2 -> CoPrime (x z1) (x z2)).
    { intros; apply H.
      apply Nat.lt_lt_succ_r.
      assumption.
      apply Nat.lt_lt_succ_r.
      assumption.
      assumption.
    }
    assert (H1: forall z : nat, z < n -> y z < x z).
    { intros.
      apply py.
      apply Nat.lt_lt_succ_r.
      assumption.
    }
    induction (Hrecn x H0 y H1).
    clear Hrecn; induction p as (H2, H3).
    assert (H4: CoPrime (prod n x) (x n)).
    { apply coPrimeProd.
      - apply H.
      - intros.
        eapply ltgt1.
        apply py.
        assumption.
    } assert (H5: y n < x n).
    { apply py.
      apply lt_n_Sn.
    }
    induction (chineseRemainderTheorem
                   (prod n x) (x n) H4 x0 (y n) H2 H5).
    exists x1; induction p as (H6, (H7, H8)).
    split.
    simpl in |- *.
    rewrite Nat.mul_comm.
    assumption.
    intros.
    induction (le_lt_or_eq z n).
    + assert
        (H10: y z =
                snd (proj1_sig (modulo (x z) (ltgt1 (y z) (x z)
                                                (H1 z H9)) x0)))
    by apply H3.
      induction (modulo (x z) (ltgt1 (y z) (x z) (H1 z H9)) x0).
      simpl in H10.
      induction (modulo (x z) (ltgt1 (y z) (x z) (py z pz)) x1).
      simpl in |- *; rewrite H10.
      induction (modulo (prod n x) (ltgt1 x0 (prod n x) H2) x1).
      simpl in H7.
      rewrite H7 in p.
      induction p1 as (H11, H12).
      induction p as (H13, H14).
      induction p0 as (H15, H16).
      rewrite H13 in H11.
      apply uniqueRem with (x z) x1.
      apply (ltgt1 (y z) (x z) (py z pz)).
      assert (divide (x z) (prod n x)).
      { apply divProd.
        assumption.
      }
      induction H17 as (x5, H17).
      rewrite H17 in H11.
      rewrite (Nat.mul_comm (x z)) in H11.
      rewrite mult_assoc in H11.
      rewrite plus_assoc in H11.
      rewrite <- mult_plus_distr_r in H11.
      exists (fst x4 * x5 + fst x2).
      split.
      apply H11.
      assumption.
      exists (fst x3); auto.
    + induction (modulo (x z) (ltgt1 (y z) (x z) (py z pz)) x1).
      induction (modulo (x n) (ltgt1 (y n) (x n) H5) x1).
      simpl in H8.
      simpl in |- *.
      rewrite H9.
      rewrite H8.
      eapply uniqueRem.
      apply (ltgt1 (y n) (x n) H5).
      exists (fst x3).
      apply p0.
      exists (fst x2).
      rewrite H9 in p.
      assumption.
    + now apply lt_n_Sm_le.
Qed.

Lemma minusS : forall a b : nat, b - a = S b - S a.
Proof. lia. Qed.

Definition Prime (n : nat) : Prop :=
  n > 1 /\ (forall q : nat, divide q n -> q = 1 \/ q = n).

Lemma primeDiv :
  forall a : nat, 1 < a ->
                  exists p : nat, Prime p /\
                                    divide p a.
Proof.
Admitted.

Lemma coPrimePrime :
 forall a b : nat,
   (forall p : nat, Prime p ->
                    ~ divide p a \/ ~ divide p b) ->
   CoPrime a b.
Proof.
Admitted.

Lemma divdec : forall n d : nat, divide d n \/ ~ divide d n.
Proof.
Admitted.

Lemma div_plus_r :
 forall a b d : nat, divide d a -> divide d (a + b) -> divide d b.
Proof.
Admitted.

Lemma div_mult_compat_l :
 forall a b c : nat, divide a b -> divide a (b * c).
Proof.
Admitted.

Lemma primedivmult :
 forall p n m : nat,
 Prime p -> divide p (n * m) -> divide p n \/ divide p m.
Proof.
Admitted.

Lemma div_trans :
 forall p q r : nat, divide p q -> divide q r -> divide p r.
Proof.
Admitted.

Lemma coPrimeSeqHelp :
 forall c i j n : nat,
 divide (factorial n) c ->
 i < j -> i <= n -> j <= n -> CoPrime (S (c * S i)) (S (c * S j)).
Proof.
  intros ? ? ? ? H H0 H1 H2.
  apply coPrimePrime.
  intros p H3.
  destruct (divdec (S (c * S i)) p) as [H4 | H4].
   assert (H5: ~ divide p c).
   { intro H5.
     assert (H6: divide p 1).
     { eapply div_plus_r.
       apply div_mult_compat_l.
       apply H5.
       rewrite plus_comm.
       simpl in |- *.
       apply H4.
     }
     induction H3 as (H3, H7).
     elim (lt_not_le _ _ H3).
     destruct H6. destruct x; lia.
   }
   destruct (divdec (S (c * S j)) p).
   assert (H7: divide p (c * (j - i))).
   { rewrite minusS.
     rewrite Nat.mul_comm.
     rewrite mult_minus_distr_r.
     rewrite (Nat.mul_comm (S j)).
     rewrite (Nat.mul_comm (S i)).
     rewrite minusS.
     destruct H4, H6. rewrite H4, H6. exists (x0 - x). nia.
   }
   destruct (primedivmult _ _ _ H3 H7).
  - elim H5.
    assumption.
  - assert (H9: j - i <= n).
    { eapply le_trans.
      apply Minus.le_minus.
      assumption.
    }
    elim H5.
    apply div_trans with (factorial n).
    apply div_trans with (j - i).
    assumption.
    unfold factorial in |- *.
    assert (H10: 1 <= j - i).
    { assert (H10: j = i + (j - i)).
      apply le_plus_minus.
      apply lt_le_weak.
      assumption.
      rewrite H10 in H0.
      lia.
    }
    replace (j - i) with (S (pred (j - i))).
    apply divProd.
    rewrite pred_of_minus.
    apply lt_S_n.
    apply le_lt_n_Sm.
    replace (S (j - i - 1)) with (1 + (j - i - 1)).
    rewrite <- le_plus_minus.
    assumption.
    assumption.
    auto.
    induction (j - i).
    elim (le_Sn_n _ H10).
    rewrite <- pred_Sn.
    reflexivity.
    assumption.
- auto.
- auto.
Qed.

Definition coPrimeBeta (z c : nat) : nat := S (c * S z).

Lemma coPrimeSeq :
  forall c i j n : nat,
    divide (factorial n) c ->
    i <> j -> i <= n -> j <= n ->
    CoPrime (coPrimeBeta i c) (coPrimeBeta j c).
Proof.
unfold coPrimeBeta in |- *.
intros ? ? ? ? H H0 H1 H2.
induction (nat_total_order _ _ H0) as [H3 | H3].
- eapply coPrimeSeqHelp.
  apply H.
  assumption.
  assumption.
  assumption.
- apply coPrimeSym.
  eapply coPrimeSeqHelp.
  + apply H.
  + assumption.
  + assumption.
  + assumption.
Qed.

Lemma gtBeta : forall z c : nat, coPrimeBeta z c > 0.
Proof.
  unfold coPrimeBeta in |- *; intros; apply gt_Sn_O.
Qed.

Fixpoint maxBeta (n: nat) (x: nat -> nat) :=
  match n with
  | 0 => 0
  | S n => Nat.max (x n) (maxBeta n x)
  end.

Lemma maxBetaLe :
  forall (n : nat) (x : nat -> nat) (i : nat),
    i < n -> x i <= maxBeta n x.
Proof.
  simple induction n.
  - intros x i H; elim (lt_n_O _ H).
  - intros; simpl in |- *; induction (le_lt_or_eq i n0).
    + eapply le_trans; [now apply H | apply Nat.le_max_r].
    + rewrite H1; apply Nat.le_max_l.
    + now apply lt_n_Sm_le.
Qed.

Theorem divProd2 :
 forall (n : nat) (x : nat -> nat) (i : nat),
 i <= n -> divide (prod i x) (prod n x).
Proof.
  simple induction n.
  - intros x i ?; assert (H0: (0 = i)) by (now apply le_n_O_eq).
    rewrite H0.
    exists 1. lia.
  - intros n0 H x i H0.
    induction (le_lt_or_eq i (S n0)).
    + simpl in |- *.
      rewrite Nat.mul_comm. assert (i <= n0) by lia.
      destruct (H x i H2).
      rewrite H3.
      exists (x0 * x n0). lia.
    + rewrite H1; exists 1; lia.
    + assumption.
Qed.

Theorem betaTheorem1 :
 forall (n : nat) (y : nat -> nat),
 {a : nat * nat |
 forall z : nat,
 z < n ->
 y z =
   snd (proj1_sig (modulo (coPrimeBeta z (snd a))
                     (gtBeta z (snd a)) (fst a)))}.
Proof.
  intros n y.
  set (c := factorial (max n (maxBeta n y))) in *.
  set (x := fun z : nat => coPrimeBeta z c) in *.
  assert
    (H: forall z1 z2 : nat,
        z1 < n -> z2 < n -> z1 <> z2 -> CoPrime (x z1) (x z2)).
  { intros; unfold x in |- *; eapply coPrimeSeq.
    - eapply div_trans.
      + unfold factorial in |- *; apply divProd2.
        apply Nat.le_max_l.
      + unfold c, factorial in |- *.
        exists 1. rewrite mult_1_r. reflexivity.
    - assumption.
    - now apply lt_le_weak.
    - apply lt_le_weak; assumption.
  }
  assert (H0: forall z : nat, z < n -> y z < x z).
  { intros; unfold x, coPrimeBeta in |- *.
    apply le_lt_n_Sm.
    induction (mult_O_le c (S z)).
    - discriminate H1.
    - apply le_trans with c.
      + unfold c in |- *.
        apply le_trans with (max n (maxBeta n y)).
        apply le_trans with (maxBeta n y).
        apply maxBetaLe.
        assumption.
        apply Nat.le_max_r.
        generalize (max n (maxBeta n y)).
        intros.
        induction n0 as [| n0 Hrecn0].
        simpl in |- *.
        apply le_n_Sn.
        induction n0 as [| n0 Hrecn1].
        simpl in |- *.
        apply le_n.
        assert (H2: factorial n0 > 0).
        { unfold factorial in |- *.
          apply prodBig1.
          intros.
          apply gt_Sn_O.
        }
        simpl in |- *.
        apply le_trans with
          (1 + (1 + n0 * (factorial n0 + n0 * factorial n0))).
        * simpl in |- *.
          repeat apply le_n_S.
          induction (mult_O_le n0 (factorial n0 + n0 * factorial n0)).
          -- unfold gt in H2.
             assert (H4: factorial n0 = factorial n0 + 0)
               by (rewrite Nat.add_comm; auto).
             rewrite H4 in H2.
             set (A1 := factorial n0 + 0) in *.
             rewrite <- H3 in H2.
             unfold A1 in H2.
             clear H4 A1.
             assert (H4: n0 * factorial n0 < 0).
             { eapply plus_lt_reg_l.
               apply H2.
             }
             elim (lt_n_O _ H4).
          -- rewrite Nat.mul_comm.
             assumption.
        * apply plus_le_compat.
          apply le_plus_trans.
          apply lt_n_Sm_le.
          apply lt_n_S.
          assumption.
          apply plus_le_compat.
          apply le_plus_trans.
          apply lt_n_Sm_le.
          apply lt_n_S.
          assumption.
          apply le_n.
      + rewrite Nat.mul_comm.
        assumption.
  }
  induction (chRem _ _ H _ H0) as [x0 [H2 H3]].
  exists (x0, c).
  intros.
  rewrite (H3 z H1).
  induction (modulo (x z) (ltgt1 (y z) (x z) (H0 z H1)) x0).
  simpl fst; simpl snd.
  destruct (modulo (coPrimeBeta z c) (gtBeta z c) x0) as [x2 p0].
  simpl in |- *.
  eapply uniqueRem.
  apply gtBeta.
  unfold x in p.
  exists (fst x1).
  apply p.
  exists (fst x2).
  apply p0.
Qed.