proposition: Lemma succ_max_distr_r n m : (maxn n m).+1 = maxn (n.+1) (m.+1).
proof: Proof. rewrite /maxn. case: leqP=>//H; case:leqP=>//. - by rewrite -[n.+1]addn1 -[m.+1]addn1 ltn_add2r ltnNge H. by rewrite ltnS leqNgt H. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)