proposition: Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.
proof: Proof. rewrite /zchinese; have [u v /= Duv _] := egcdzP m1 m2. rewrite -{2}[r1]mulr1 -((gcdz _ _ =P 1) co_m12) -Duv. by rewrite mulrDr mulrAC addrC (mulrAC r2) !mulrA !modzMDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)