proposition: Lemma Rmult_le_lt_reg_l : forall a b c d, 0 < a -> a * b <= a * c < a * d -> b <= c < d.
proof: Proof. intros a b c d Ha H. split. now apply Rmult_le_reg_l with (1 := Ha). now apply Rmult_lt_reg_l with (1 := Ha). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core) Gappa(Gappa_tactic)