proposition: Lemma eq_existsb_in D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [exists (x | D x), P1 x] = [exists (x | D x), P2 x].
proof: Proof. by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)