proposition: Lemma odivr_mul2l a b c : a != 0 -> b != 0 -> a * b %/? (a * c) = (b %/? c).
proof: Proof. move=> a0 b0. case c0: (c == 0); first by rewrite (eqP c0) mulr0 !odivr0 // mulf_neq0. case: odivrP=> [x|H]. rewrite mulrCA; move/(mulfI a0). case: (odivrP b c)=> [x' ->|H]; first by move/(mulIf (negbT c0)) ->. by move=> Hbxc; move: (H x); rewrite Hbxc eqxx. by case: odivrP=> //x Hbxc; move: (H x); rewrite mulrCA Hbxc eqxx. 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