proposition: Lemma Rmult_min_distr_r : forall a b c, 0 <= a -> Rmin b c * a = Rmin (b * a) (c * a).
proof: Proof. intros a b c. rewrite <- 3!(Rmult_comm a). apply Rmult_min_distr_l. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)