proposition: Lemma partitionsP p E: inc p (partitions E) <-> partition_s p E.
proof: Proof. split; [by move/Zo_hi|move => h;apply/Zo_i=> //;apply /setP_P => t ty ]. by move:h=> [[<- _] _ ]; apply/setP_P; apply: setU_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)