proposition: Lemma extendible_to_n:forall B', Subset B' town -> cardinal B' <= n -> {B:t| cardinal B = n /\ Subset B' B /\ Subset B town}.
proof: Proof. intros B' H_sub H_B'_cardinal. assert (H_cardinal_aux_3:2*n<=(cardinal town)-1);[apply le_trans with (2*n); omega|]. clear property. induction n in H_B'_cardinal, H_cardinal_aux_3 |- *. generalize (sym_eq (le_n_O_eq _ H_B'_cardinal)); intro H_eq. generalize (empty_is_empty_1 (cardinal_inv_1 H_eq)). intro H_B'. exists empty; repeat split. rewrite H_B'; apply subset_empty. apply subset_empty. destruct (le_lt_eq_dec _ _ H_B'_cardinal) as [H_lt|H_le]. generalize (lt_n_Sm_le _ _ H_lt); clear H_lt; intro H_le. assert (H_cardinal_town_2:2 * n0 <= cardinal town - 1);[omega|]. destruct (IHn0 H_le H_cardinal_town_2) as [C [HC1 [HC2 HC3]]]. assert (HC5:cardinal C <= cardinal town - 1). rewrite HC1; apply le_trans with (2*(S n0));[omega| assumption]. destruct (extendible_by_one C HC5) as [d [Hd1 Hd2]]. exists (d ++ C). repeat split. rewrite (add_cardinal_2 Hd2); rewrite HC1; reflexivity. apply subset_add_2; assumption. apply subset_add_3; assumption. exists B'. repeat split; trivial; apply subset_refl. Qed.
imports: Arith Omega