proposition: Lemma eqCmod_nat (e m n : nat) : (m == n %[mod e])%C = (m == n %[mod e]).
proof: Proof. without loss lenm: m n / (n <= m)%N. by move=> IH; case/orP: (leq_total m n) => /IH //; rewrite eqCmod_sym eq_sym. by rewrite /eqCmod -natrB // dvdC_nat eqn_mod_dvd. 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)