proposition: Lemma eq_xchoose P Q exP exQ : P =1 Q -> @xchoose P exP = @xchoose Q exQ.
proof: Proof. rewrite /xchoose => eqPQ. case: (xchoose_subproof exP) => x; case: (xchoose_subproof exQ) => y /=. case: ex_minnP => n; rewrite -(extensional eqPQ) => Pn minQn. case: ex_minnP => m; rewrite !(extensional eqPQ) => Qm minPm. by case: (eqVneq m n) => [-> -> [] //|]; rewrite eqn_leq minQn ?minPm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)