proposition: Lemma Sperner_p4 A: inc A (free_subsets r) <-> sub A (\Po E) /\ free_subset r A.
proof: Proof. move: (subp_osr E) => [or sr]; rewrite/free_subsets sr. by split;[ move/Zo_P => [/setP_P] | move => [/setP_P ha hb0]; apply: Zo_i]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)