proposition: Lemma eq_ex_maxn (P Q : pred nat) m n exP ubP exQ ubQ : P =1 Q -> @ex_maxn P m exP ubP = @ex_maxn Q n exQ ubQ.
proof: Proof. move=> eqPQ; case: ex_maxnP => i Pi max_i; case: ex_maxnP => j Pj max_j. by apply/eqP; rewrite eqn_leq max_i ?eqPQ // max_j -?eqPQ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring