proposition: Fact addNq : left_inverse (fracq (0, 1)) oppq addq.
proof: Proof. move=> x; rewrite -[x]valqK !(addq_frac, oppq_frac) ?denq_neq0 //. rewrite !addq_subdefE /oppq_subdef //= mulNr addNr; apply/eqP. by rewrite fracq_eq ?mulf_neq0 ?denq_neq0 //= !mul0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)