proposition: Lemma Rdiv_lt_mult_pos a b c : (0 < b -> a * b < c -> a < c / b)%R.
proof: Proof. intros Hb Hab. apply (Rmult_lt_reg_r b _ _ Hb). now unfold Rdiv; rewrite Rmult_assoc, Rinv_l, Rmult_1_r; lra. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic