proposition: Lemma Rle_mult_Rlt : forall c a b : R, 0 < b -> c < 1 -> a <= b*c -> a < b.
proof: Proof. intros. apply Rle_lt_trans with (1 := H1). pattern b at 2 ; rewrite <-(Rmult_1_r b). apply Rmult_lt_compat_l ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)