proposition: Lemma leq_max m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2).
proof: Proof. wlog le_n21: n1 n2 / n2 <= n1 => [th_sym|]. by case/orP: (leq_total n2 n1) => /th_sym; last rewrite maxnC orbC. by rewrite (maxn_idPl le_n21) orb_idr // => /leq_trans->. Qed.
imports: mathcomp(all_ssreflect)