proposition: Lemma mulV_l : forall a, a != 0%:F -> mul (inv a) a = 1%:F.
proof: Proof. elim/quotW=> x /=; rewrite !piE. rewrite /equivf !numden_Ratio ?oner_eq0 // mulr1 mulr0=> nx0. apply/eqmodP; rewrite /= equivfE. by rewrite !numden_Ratio ?(oner_eq0, mulf_neq0, domP) // !mulr1 mulrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)