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