proposition: Lemma IdomainMixin (R : unitRingType): Field.axiom R -> IntegralDomain.axiom R.
proof: Proof. move=> m x y xy0; apply/norP=> [[]] /m Ux /m. by rewrite -(unitrMr _ Ux) xy0 unitr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)