proposition: Lemma Rmult_min_distr_l : forall a b c, 0 <= a -> a * Rmin b c = Rmin (a * b) (a * c).
proof: Proof. intros a b c Ha. destruct Ha as [Ha|Ha]. unfold Rmin. case Rle_dec ; intros H. apply (Rmult_le_compat_l _ _ _ (Rlt_le _ _ Ha)) in H. case Rle_dec ; intuition. apply Rnot_le_lt, (Rmult_lt_compat_l _ _ _ Ha), Rlt_not_le in H. case Rle_dec ; intuition. rewrite <- Ha ; clear a Ha. repeat rewrite Rmult_0_l. unfold Rmin ; assert (H := Rle_refl 0). case Rle_dec ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)