proposition: Lemma Rdiv_le_l : forall a b c, 0 < a -> b <= c / a -> a * b <= c.
proof: Proof. intros a b c Ha Hb. apply Rmult_le_reg_r with (/a). now apply Rinv_0_lt_compat. replace (a * b * /a) with b. exact Hb. field. now apply Rgt_not_eq. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core) Gappa(Gappa_tactic)