proposition: Lemma chinese_mod x : x = chinese (x %% m1) (x %% m2) %[mod m1 * m2].
proof: Proof. apply/eqP; rewrite chinese_remainder //. by rewrite chinese_modl chinese_modr !modn_mod !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)