proposition: Lemma eqCmodD e x1 x2 y1 y2 : (x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 + y1 == x2 + y2 %[mod e])%C.
proof: Proof. by rewrite -(eqCmodDl e x2 y1) -(eqCmodDr e y1); apply: eqCmod_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)