proposition: Lemma extendible_by_one:forall B', cardinal B' <= (cardinal town)-1 -> {d:elt| In d town /\ ~(In d B')}.
proof: Proof. clear knows knows_sym knows_extensional property. intros B' H_cardinal_town. assert (H_town:1<=(cardinal town)); [omega|]. rewrite <- (diff_inter_cardinal town B') in H_cardinal_town. rewrite <- (diff_inter_cardinal town B') in H_town. assert (H_inter:cardinal (inter town B') <= cardinal B'); [apply (subset_cardinal);apply (inter_subset_2)|]. generalize (le_trans _ _ _ H_inter H_cardinal_town); intro H1. assert (H2:1<=cardinal (diff 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