proposition: Remark subsets_2: forall B : t, Subset B town_2 -> cardinal B = 2 -> {B [=] 1++2++empty}+{B[=]1++3++empty}+{B[=]1++4++empty}+{B [=] 1++5++empty}+{B[=]2++3++empty}+ {B[=]2++4++empty}+{B[=]2++5++empty}+{B[=]3++4++empty}+{B [=] 3++5++empty}+{B[=]4++5++empty}.
proof: Proof. intros B H_sub H_card. destruct (In_dec 1 B) as [H1|H1]. do 6 left. assert (H_card_rem:cardinal (remove 1 B)=1); [ rewrite <- (remove_cardinal_1 H1) in H_card; apply eq_add_S; assumption|]. destruct (In_dec 2 (remove 1 B)) as [H12|H12]. do 3 left. rewrite <- (add_remove H1). rewrite <- (add_remove H12). generalize (remove_cardinal_1 H12). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 3 (remove 1 B)) as [H13|H13]. do 2 left; right. rewrite <- (add_remove H1). rewrite <- (add_remove H13). generalize (remove_cardinal_1 H13). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 4 (remove 1 B)) as [H14|H14]. left; right. rewrite <- (add_remove H1). rewrite <- (add_remove H14). generalize (remove_cardinal_1 H14). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 5 (remove 1 B)) as [H15|H15]. right. rewrite <- (add_remove H1). rewrite <- (add_remove H15). generalize (remove_cardinal_1 H15). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... apply False_rec. assert (H11:=(@remove_1 B _ _ (refl_equal 1))). destruct (cardinal_inv_2 H_card_rem) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H11; rewrite Hb1 in Hb; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H12; rewrite <- Hb2; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H13; rewrite <- Hb3; assumption. destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4]. apply H14; rewrite <- Hb4; assumption. destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5]. apply H15; rewrite <- Hb5; assumption. assert (H_sub':=@subset_remove_3 _ _ 1 H_sub). assert (Hb_town:=H_sub' _ Hb). unfold town_2 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. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply Hb4; rewrite Hb4_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply Hb5; rewrite Hb5_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb5_town)... destruct (In_dec 2 B) as [H2|H2]. assert (H_card_rem:cardinal (remove 2 B)=1); [ rewrite <- (remove_cardinal_1 H2) in H_card; apply eq_add_S; assumption|]. assert (H21:=fun HH : In 1 (remove 2 B) => H1 (remove_3 HH)). destruct (In_dec 3 (remove 2 B)) as [H23|H23]. do 5 left; right. rewrite <- (add_remove H2). rewrite <- (add_remove H23). generalize (remove_cardinal_1 H23). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 4 (remove 2 B)) as [H24|H24]. do 4 left; right. rewrite <- (add_remove H2). rewrite <- (add_remove H24). generalize (remove_cardinal_1 H24). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 5 (remove 2 B)) as [H25|H25]. do 3 left; right. rewrite <- (add_remove H2). rewrite <- (add_remove H25). generalize (remove_cardinal_1 H25). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... apply False_rec. assert (H22:=(@remove_1 B _ _ (refl_equal 2))). destruct (cardinal_inv_2 H_card_rem) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H21; rewrite Hb1 in Hb; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H22; rewrite Hb2 in Hb; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H23; rewrite <- Hb3; assumption. destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4]. apply H24; rewrite <- Hb4; assumption. destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5]. apply H25; rewrite <- Hb5; assumption. assert (H_sub':=@subset_remove_3 _ _ 2 H_sub). assert (Hb_town:=H_sub' _ Hb). unfold town_2 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. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply Hb4; rewrite Hb4_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply Hb5; rewrite Hb5_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb5_town)... destruct (In_dec 3 B) as [H3|H3]. assert (H_card_rem:cardinal (remove 3 B)=1); [ rewrite <- (remove_cardinal_1 H3) in H_card; apply eq_add_S; assumption|]. assert (H31:=fun HH : In 1 (remove 3 B) => H1 (remove_3 HH)). assert (H32:=fun HH : In 2 (remove 3 B) => H2 (remove_3 HH)). destruct (In_dec 4 (remove 3 B)) as [H34|H34]. do 2 left; right. rewrite <- (add_remove H3). rewrite <- (add_remove H34). generalize (remove_cardinal_1 H34). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... destruct (In_dec 5 (remove 3 B)) as [H35|H35]. left; right. rewrite <- (add_remove H3). rewrite <- (add_remove H35). generalize (remove_cardinal_1 H35). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... apply False_rec. assert (H33:=(@remove_1 B _ _ (refl_equal 3))). destruct (cardinal_inv_2 H_card_rem) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H31; rewrite Hb1 in Hb; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H32; rewrite Hb2 in Hb; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H33; rewrite Hb3 in Hb; assumption. destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4]. apply H34; rewrite <- Hb4; assumption. destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5]. apply H35; rewrite <- Hb5; assumption. assert (H_sub':=@subset_remove_3 _ _ 3 H_sub). assert (Hb_town:=H_sub' _ Hb). unfold town_2 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. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply Hb4; rewrite Hb4_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply Hb5; rewrite Hb5_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb5_town)... destruct (In_dec 4 B) as [H4|H4]. assert (H_card_rem:cardinal (remove 4 B)=1); [ rewrite <- (remove_cardinal_1 H4) in H_card; apply eq_add_S; assumption|]. assert (H41:=fun HH : In 1 (remove 4 B) => H1 (remove_3 HH)). assert (H42:=fun HH : In 2 (remove 4 B) => H2 (remove_3 HH)). assert (H43:=fun HH : In 3 (remove 4 B) => H3 (remove_3 HH)). destruct (In_dec 5 (remove 4 B)) as [H45|H45]. right. rewrite <- (add_remove H4). rewrite <- (add_remove H45). generalize (remove_cardinal_1 H45). rewrite H_card_rem; intro H_eq2. rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity... apply False_rec. assert (H44:=(@remove_1 B _ _ (refl_equal 4))). destruct (cardinal_inv_2 H_card_rem) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H41; rewrite Hb1 in Hb; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H42; rewrite Hb2 in Hb; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H43; rewrite Hb3 in Hb; assumption. destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4]. apply H44; rewrite Hb4 in Hb; assumption. destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5]. apply H45; rewrite <- Hb5; assumption. assert (H_sub':=@subset_remove_3 _ _ 4 H_sub). assert (Hb_town:=H_sub' _ Hb). unfold town_2 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. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply Hb4; rewrite Hb4_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply Hb5; rewrite Hb5_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb5_town)... apply False_rec. destruct (In_dec 5 B) as [H5|H5]. assert (H_card_rem:cardinal (remove 5 B)=1); [ rewrite <- (remove_cardinal_1 H5) in H_card; apply eq_add_S; assumption|]. assert (H51:=fun HH : In 1 (remove 5 B) => H1 (remove_3 HH)). assert (H52:=fun HH : In 2 (remove 5 B) => H2 (remove_3 HH)). assert (H53:=fun HH : In 3 (remove 5 B) => H3 (remove_3 HH)). assert (H54:=fun HH : In 4 (remove 5 B) => H4 (remove_3 HH)). assert (H55:=(@remove_1 B _ _ (refl_equal 5))). destruct (cardinal_inv_2 H_card_rem) as [b Hb]. assert (H_sub':=@subset_remove_3 _ _ 5 H_sub). assert (Hb_town:=H_sub' _ Hb). unfold town_2 in Hb_town. destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town]. apply H51; rewrite <- Hb1_town in Hb; assumption. destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town]. apply H52; rewrite <- Hb2_town in Hb; assumption. destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town]. apply H53; rewrite <- Hb3_town in Hb; assumption. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply H54; rewrite <- Hb4_town in Hb; assumption. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply H55; rewrite <- Hb5_town in Hb; assumption. apply (proj1 (FM.empty_iff b) Hb5_town)... destruct (cardinal_inv_2 H_card) as [b Hb]. destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1]. apply H1; rewrite Hb1 in Hb; assumption. destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2]. apply H2; rewrite Hb2 in Hb; assumption. destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3]. apply H3; rewrite Hb3 in Hb; assumption. destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4]. apply H4; rewrite Hb4 in Hb; assumption. destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5]. apply H5; rewrite <- Hb5; assumption. assert (Hb_town:=H_sub _ Hb). unfold town_2 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. destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town]. apply Hb4; rewrite Hb4_town; reflexivity. destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town]. apply Hb5; rewrite Hb5_town; reflexivity. apply (proj1 (FM.empty_iff b) Hb5_town)... Qed.
imports: AMM11262