proposition: Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) : {in p, forall x, P x /\ Q x} <-> {in p, forall x, P x} /\ {in p, forall x, Q x}.
proof: Proof. split=> [cnd|[cnd1 cnd2] x xin]; first by split=> x xin; case: (cnd x xin). by split; [apply: cnd1 | apply: cnd2]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed