proposition: 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 (div_eucl x1 (ltgt1 _ _ pa) y)) /\ b = snd (proj1_sig (div_eucl x2 (ltgt1 _ _ pb) y))}.
proof: Proof. intros ? ? H a b pa pb. destruct (le_lt_dec a b). - apply chineseRemainderTheoremHelp; assumption. - assert (H0: b <= a) by (now apply Nat.lt_le_incl). 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.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow