proposition: Lemma numer0 x : (\n_x == 0) = (x == (ratio0 R) %[mod_eq equivf]).
proof: Proof. by rewrite eqmodE /= !equivfE // mulr1 mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)