proposition: Lemma divRM (r1 r2 x : R) : r1 != 0 -> r2 != 0 -> x / (r1 * r2) = x / r1 * / r2.
proof: Proof. by move=> ? ?; rewrite {1}/Rdiv invRM // mulRA. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)