proposition: Lemma powerset_inter: {morph powerset : A B / A \cap B}.
proof: Proof. move => A B; apply: extensionality. apply: intersection_greatest; apply: powerset_mono. apply: subsetI2l. apply:subsetI2r. move=> x /setI2_P[] /setP_P xpA /setP_P xpB; apply /setP_P. by apply: intersection_greatest. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)