proposition: 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 (div_eucl x1 (ltgt1 _ _ pa) y)) /\ b = snd (proj1_sig (div_eucl x2 (ltgt1 _ _ pb) y))}.
proof: 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). { change 0 with (0 * x2). unfold gt in |- *; rewrite Nat.mul_comm. rewrite (Nat.mul_comm x1). induction x2 as [| x2 Hrecx2]. elim (Nat.nlt_0_r _ pb). rewrite <- (Nat.mul_lt_mono_pos_l (S _)). fold (x1 > 0) in |- *. eapply ltgt1. apply pa. auto. auto with arith. } 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 (div_eucl 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 (div_eucl 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.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow