proposition: Lemma eqAmodM e : {in Aint &, forall x1 y2 x2 y1, x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 * y1 == x2 * y2 %[mod e]}%A.
proof: Proof. move=> x1 y2 Zx1 Zy2 x2 y1 eq_x /(eqAmodMl Zx1)/eqAmod_trans-> //. exact: eqAmodMr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)