proposition: Lemma extendible_by_one:∀ B', |B'| ≤ |town| -1 ⇒ ∃d, d∈town ∧ ¬(d∈B').
proof: Proof. clear knows knows_sym knows_extensional property. intros B' H_cardinal_town. assert (H_town:1≤ |town|); [omega|]. rewrite <- (diff_inter_cardinal town B') in H_cardinal_town. rewrite <- (diff_inter_cardinal town B') in H_town. assert (H_inter:|town∩B'| ≤ |B'|); [apply (subset_cardinal);apply (inter_subset_2)|]. generalize (le_trans _ _ _ H_inter H_cardinal_town); intro H1. assert (H2:1≤|town\B'|); [omega|]. assert (H3:=(S_pred _ _ H2)). destruct (cardinal_inv_2 H3) as [d Hd]. exists d; split. apply diff_1 with B'; assumption. apply diff_2 with town; assumption. Qed.
imports: Arith Omega