proposition: Lemma Rmin_trans : forall a b c : R, (c <= Rmin a b)%R -> (c <= a)%R /\ (c <= b)%R.
proof: Proof. intros a b c H. split. exact (Rle_trans _ _ _ H (Rmin_l _ _)). exact (Rle_trans _ _ _ H (Rmin_r _ _)). Qed.
imports: Reals