proposition: Lemma plus_max_distr_l m n p: maxn (p + n) (p + m) = p + maxn n m.
proof: Proof. rewrite /maxn. case: leqP=>// H1; case: leqP=>//. - suff: m <= n by rewrite ltnNge=>H; move/negP. by rewrite leq_add2l in H1. suff: n < m by move=>H; rewrite leqNgt H. by rewrite ltn_add2l in H1. Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype)