proposition: Lemma divR_neq0' (x y : R) : x != 0 -> y != 0 -> x / y != 0.
proof: Proof. by move => x0 y0; rewrite mulR_neq0' x0 /= invR_neq0'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)