proposition: Lemma Rplus_max_distr_l : forall a b c, a + Rmax b c = Rmax (a + b) (a + c).
proof: Proof. intros a b c. unfold Rmax. case Rle_dec ; intros H ; case Rle_dec ; intros H' ; try easy. elim H'. apply Rplus_le_compat_l with (1 := H). elim H. apply Rplus_le_reg_l with (1 := H'). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)