proposition: Lemma eqR_divr_mulr z x y : z != 0 -> (y / z = x) <-> (y = x * z).
proof: Proof. move=> z0; split => [<-|->]; first by rewrite -mulRA mulVR // mulR1. by rewrite /Rdiv -mulRA mulRV // mulR1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)