proposition: Lemma mod0r a : 0 %% a = 0.
proof: Proof. have [-> | a0] := eqVneq a 0; first by rewrite modr0. case: edivP=> q r; rewrite a0 /= => /eqP. rewrite eq_sym (can2_eq (@addKr _ _) (@addNKr _ _)) addr0 => /eqP->. rewrite -mulNr; apply: contraTeq; rewrite -leqNgt. by move/leq_norm; apply; exact: dvdr_mull. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete