proposition: Lemma free_rep_prop1 A: inc A (free_subsets r) -> exists2 f, free_rep f & target f = A.
proof: Proof. move => h. move:(h) => /Sperner_p4/proj1/sub_smaller; rewrite card_setP- cpowcr => h'. move: (NS_le_nat h' (NS_pow NS2 Sperner_p0)) => caN. case: (equipotent_ex_pr1(double_cardinal A)). set f := equipotent_ex _ _; move => bf sf tf. exists f => //; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)