proposition: Lemma chinese_modr r1 r2 : chinese r1 r2 = r2 %[mod m2].
proof: Proof. rewrite /chinese; case: (posnP m1) co_m12 => [-> /eqnP | m1_gt0 _]. by rewrite gcd0n => ->; rewrite !modn1. case: (egcdnP m2) => // k1 k2 def_m2 _. rewrite addnC mulnAC -mulnA def_m2 (eqnP co_m12) mulnDr mulnA muln1. by rewrite addnAC (mulnAC _ m2) -mulnDl modnMDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)