proposition: Lemma RinvE' (x : R) : (/ x)%coqR = (x^-1)%mcR.
proof: Proof. have [-> | ] := eqVneq x 0%coqR; last exact: RinvE. rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=. rewrite RinvImpl.Rinv_def. case: (Req_appart_dec 0 R0) => //. by move=> /[dup] -[] => /RltP; rewrite Order.POrderTheory.ltxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)