proposition: Lemma Rcompare_div_l x y z : (0 < y)%R -> Rcompare (x / y) z = Rcompare x (y * z).
proof: Proof. intro yP. replace x with (y * (x / y))%R at 2. now rewrite Rcompare_mult_l. field; lra. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic