proposition: Lemma eq_choose P Q : P =1 Q -> choose P =1 choose Q.
proof: Proof. rewrite /choose => eqPQ x0. do [case: insubP; rewrite eqPQ] => [[x Px] Qx0 _| ?]; last by rewrite insubN. by rewrite insubT; apply: eq_xchoose. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)