proposition: Remark acquintance_2: ∀ B, B⊆town_2 ⇒ |B| = 2 ⇒ ∃d, d∈(town_2\B) ∧ (∀ b, b∈B ⇒ d ℛ₂ b).
proof: Proof. intros B H_sub H_card. destruct (subsets_2 B H_sub H_card) as [[[[[[[[[HB12|HB13]|HB14]|HB15]|HB23]|HB24]|HB25]|HB34]|HB35]|HB45]. exists 5; split. rewrite HB12; apply mem_2; trivial. intro b; rewrite HB12; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 4; split. rewrite HB13; apply mem_2; trivial. intro b; rewrite HB13; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 3; split. rewrite HB14; apply mem_2; trivial. intro b; rewrite HB14; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 2; split. rewrite HB15; apply mem_2; trivial. intro b; rewrite HB15; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 5; split. rewrite HB23; apply mem_2; trivial. intro b; rewrite HB23; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 1; split. rewrite HB24; apply mem_2; trivial. intro b; rewrite HB24; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 1; split. rewrite HB25; apply mem_2; trivial. intro b; rewrite HB25; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 1; split. rewrite HB34; apply mem_2; trivial. intro b; rewrite HB34; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 1; split. rewrite HB35; apply mem_2; trivial. intro b; rewrite HB35; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). exists 3; split. rewrite HB45; apply mem_2; trivial. intro b; rewrite HB45; intro Hb. destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H]. compute in H; rewrite <- H; simpl; trivial. destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H']. compute in H'; rewrite <- H'; simpl; trivial. apply False_ind; apply (proj1 (FM.empty_iff b) H'). Defined.
imports: utf_AMM11262