fact: Definition integral_domain_axiom (R : ringType) := forall x y : R, x * y = 0 -> (x == 0) || (y == 0).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)