proposition: Remark acquintance_1: ∀ B, B⊆town_1 ⇒ |B| = 1 ⇒ ∃d, d∈(town_1\B) ∧ (∀ b, b∈B ⇒ d ℛ₁ b).
proof: Proof. intros B H_sub H_card. destruct (subsets_1 B H_sub H_card) as [[HB1|HB2]|HB3]. exists 2; split. rewrite HB1; apply mem_2; trivial. intro b; rewrite HB1; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). exists 1; split. rewrite HB2; apply mem_2; trivial. intro b; rewrite HB2; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). exists 2; split. rewrite HB3; apply mem_2; trivial. intro b; rewrite HB3; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H). Defined.
imports: utf_AMM11262