proposition: Lemma divr_mulKr a b : b != 0 -> (b * a) %/ b = a.
proof: Proof. move=> H. have: (b * a) %% b = 0. by apply/eqP; rewrite modr_eq0 dvdr_mulr // dvdrr. rewrite /divr /modr. case: edivrP=> c r He Hb /= Hr. rewrite Hr addr0 mulrC in He. by apply: (mulIf H). 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