proposition: 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 (div_eucl (x z) (ltgt1 _ _ (py z pz)) a)))}.
proof: Proof. intro. induction n as [| n Hrecn]. - intros; exists 0. split. + simpl in |- *. apply Nat.lt_0_succ. + intros. elim (Nat.nlt_0_r _ 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 Nat.lt_succ_diag_r. } 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. assert (lezn : z <= n) by lia. rewrite Nat.lt_eq_cases in lezn. destruct lezn. + assert (H10: y z = snd (proj1_sig (div_eucl (x z) (ltgt1 (y z) (x z) (H1 z H9)) x0))) by apply H3. induction (div_eucl (x z) (ltgt1 (y z) (x z) (H1 z H9)) x0). simpl in H10. induction (div_eucl (x z) (ltgt1 (y z) (x z) (py z pz)) x1). simpl in |- *; rewrite H10. induction (div_eucl (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 Nat.mul_assoc in H11. rewrite Nat.add_assoc in H11. rewrite <- Nat.mul_add_distr_r in H11. exists (fst x4 * x5 + fst x2). split. apply H11. assumption. exists (fst x3); auto. + induction (div_eucl (x z) (ltgt1 (y z) (x z) (py z pz)) x1). induction (div_eucl (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. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow