(* Show that each nonempty set has as many subsets of even cardinal as subsets of odd cardinal. *) (* The idea consists in re-indexing the sums (use 2j and 2j+1 instead of a predicate) and extending the sum (if j is big enough, bin_small says that C(n,2j)=0). Hence the first step consists in proving *) Lemma Exercise5_2a n: n > 0 -> \sum_(i