cardinal_3_bis.v

Lemma Add_transpose_neqkey : forall k1 k2 e1 e2 m1 m2 m3,
  ~ E.eq k1 k2 -> Add k1 e1 m1 m2 -> Add k2 e2 m2 m3 ->
  { m | Add k2 e2 m1 m /\ Add k1 e1 m m3 }.
Proof.
  intros k1 k2 e1 e2 m1 m2 m3 k_neq Add_1 Add_2.
  exists (add k2 e2 m1).
  split; [easy|].
  unfold Add; intros k.
  rewrite Add_2, add_o, Add_1, !add_o.
  destruct (eq_dec k1 k), (eq_dec k2 k); try reflexivity.
  contradiction k_neq. eauto.
Qed.

Lemma cardinal_Add_In:
  forall m m' x e, In x m -> Add x e m m' -> cardinal m' = cardinal m.
Proof.
  intros m. induction m as [m Hm|m1 m2 IH x e x_In x_Add] using map_induction.
  - intros m' x e x_In x_Add.
    destruct x_In as (e' & x_MapsTo).
    contradiction (Hm _ _ x_MapsTo).
  - intros m' x' e' x'_In x'_Add.
    destruct (E.eq_dec x x').
    + assert (Add x e' m1 m') as Ha.
      { intro y.
        rewrite e0, x'_Add, add_o, x_Add, !add_o.
        destruct (eq_dec x y), (eq_dec x' y) as [|neq]; try reflexivity.
        contradiction neq; eauto.
      }
      erewrite cardinal_2 with (m':=m') by eassumption.
      erewrite cardinal_2 with (m':=m2) by eassumption.
      reflexivity.
    + edestruct Add_transpose_neqkey
        as [ m_tsp [ Add_tsp_1 Add_tsp_2 ] ]; try eassumption.
      assert (In x' m1) as Ha.
      { erewrite in_find_iff, <- add_neq_o, <- x_Add, <- in_find_iff;
          assumption.
      }
      assert (~ In x m_tsp) as Hb.
      { rewrite not_find_in_iff, Add_tsp_1, add_neq_o, <- not_find_in_iff;
          eauto.
      }
      erewrite cardinal_2 with (m':=m') by eassumption.
      erewrite cardinal_2 with (m:=m1) (m':=m2) by eassumption.
      erewrite IH by eassumption.
      reflexivity.
Qed.