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