proposition: Lemma invR_eq0 (x : R) : / x = 0 -> x = 0.
proof: Proof. move/eqP=> H; apply/eqP; apply: contraTT H => H; exact/eqP/invR_neq0/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)