proposition: Lemma addN_l : left_inverse 0%:F opp add.
proof: Proof. elim/quotW=> x; apply/eqP; rewrite piE /equivf. rewrite /addf /oppf !numden_Ratio ?(oner_eq0, mulf_neq0, domP) //. by rewrite mulr1 mulr0 mulNr addNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)