proposition: Lemma invRM (r1 r2 : R) : r1 != 0 -> r2 != 0 -> / (r1 * r2) = / r1 * / r2.
proof: Proof. by move=> /eqP r10 /eqP r20; rewrite Rinv_mult. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)