proposition: Lemma odivP a b : div_spec a b (odiv a b).
proof: Proof. rewrite /odiv; case: edivP=> q r -> hr. case r0: (r == 0)=> //=; constructor. by rewrite (eqP r0) addr0; case: ifP=> //; move/eqP->; rewrite !mulr0. move=> x; case b0: (b == 0) hr=> /= hr. by rewrite (eqP b0) !mulr0 add0r r0. rewrite addrC (can2_eq (@addrK _ _) (@addrNK _ _)) -mulrBl. case xq : (x - q == 0); first by rewrite (eqP xq) mul0r r0. by apply: contraL hr; rewrite -leqNgt; move/eqP->; rewrite norm_mul ?xq. 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