proposition: 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: Proof. intros. exists (add k2 e2 m1). split. easy. unfold Add; intros. rewrite H1. destruct (E.eq_dec k1 y). - assert (~ E.eq k2 y). contradict H. apply E.eq_trans with (y:=y); auto. now rewrite add_neq_o, add_eq_o, H0, add_eq_o by assumption. - destruct (E.eq_dec k2 y). + now rewrite add_eq_o, add_neq_o, add_eq_o by assumption. + now rewrite add_neq_o, H0, add_neq_o, add_neq_o, add_neq_o by assumption. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface