proposition: Lemma Rcompare_div_r x y z : (0 < z)%R -> Rcompare x (y / z) = Rcompare (z * x) y.
proof: Proof. intro yP. rewrite Rcompare_sym, Rcompare_div_l, Rcompare_sym; try easy. now destruct Rcompare. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic