proposition: Lemma max_is_max m n: n <= maxn m n /\ m <= maxn m n.
proof: Proof. rewrite /maxn. case: leqP=>//. move=>H; split. by apply: leqnn. by rewrite ltn_neqAle in H; case/andP: H. Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype)