proposition: Theorem Rmult_min_distr_l : forall r r1 r2 : R, (0 <= r)%R -> (r * Rmin r1 r2)%R = Rmin (r * r1) (r * r2).
proof: Proof. intros r r1 r2 Hr. rewrite 3!(Rmult_comm r). now apply Rmult_min_distr_r. Qed.
imports: Coq(Psatz Reals ZArith) Zaux