proposition: Lemma ex_maxnP : ex_maxn_spec ex_maxn.
proof: Proof. rewrite /ex_maxn; case: ex_minnP => i Pmi min_i; split=> // j Pj. have le_i_mj: i <= m - j by rewrite min_i // subKn // ubP. rewrite -subn_eq0 subnBA ?(leq_trans le_i_mj) ?leq_subr //. by rewrite addnC -subnBA ?ubP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring