proposition: Lemma Rmax_le_Rplus : forall a b : R, 0 <= a -> 0 <= b -> Rmax a b <= a + b.
proof: Proof. intros. destruct (Rle_lt_dec a b). rewrite <- (Rplus_0_l (Rmax a b)). rewrite Rmax_right. apply Rplus_le_compat_r. apply H. apply r. rewrite <- (Rplus_0_r (Rmax a b)). rewrite Rmax_left. apply Rplus_le_compat_l. apply H0. apply Rlt_le, r. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)