proposition: Remark subsets_1: forall B : t, Subset B town_1 -> cardinal B = 1 -> {B [=] 1++empty}+{B[=]2++empty}+{B[=]3++empty}.
proof: Proof. intros B H_sub H_card. destruct (In_dec 1 B) as [H1|H1]. left; left; rewrite <- (add_remove H1); generalize (remove_cardinal_1 H1); rewrite H_card; intro H_eq; rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity... destruct (In_dec 2 B) as [H2|H2]. left; right; rewrite <- (add_remove H2); generalize (remove_cardinal_1 H2); rewrite H_card; intro H_eq; rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity... destruct (In_dec 3 B) as [H3|H3]. right; rewrite <- (add_remove H3); generalize (remove_cardinal_1 H3); rewrite H_card; intro H_eq; rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity... apply False_rec. destruct (cardinal_inv_2 H_card) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H1; rewrite <- Hb1; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H2; rewrite <- Hb2; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H3; rewrite <- Hb3; assumption. assert (Hb_town:=H_sub _ Hb). unfold town_1 in Hb_town. destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town]. apply Hb1; rewrite Hb1_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town]. apply Hb2; rewrite Hb2_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town]. apply Hb3; rewrite Hb3_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb3_town). Qed.
imports: AMM11262