proposition: Lemma choose_id P x0 y0 : P x0 -> P y0 -> choose P x0 = choose P y0.
proof: Proof. by move=> Px0 Py0; rewrite /choose !insubT /=; apply: eq_xchoose. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)