proposition: Lemma Rmax_trans : forall a b c : R, (Rmax a b <= c)%R -> (a <= c)%R /\ (b <= c)%R.
proof: Proof. intros a b c H. split. exact (Rle_trans _ _ _ (RmaxLess1 _ _) H). exact (Rle_trans _ _ _ (RmaxLess2 _ _) H). Qed.
imports: Reals