proposition: Lemma chinese_remainder x y : (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
proof: Proof. wlog le_yx : x y / y <= x; last by rewrite !eqn_mod_dvd // Gauss_dvd. by have [?|/ltnW ?] := leqP y x; last rewrite !(eq_sym (x %% _)); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)