proposition: Lemma find_add_inv : ∀ f g (fg : N) x y z m, M.find (f, g) (M.add (x, y) z m) = Some fg -> (x = f ∧ y = g ∧ z = fg) ∨ M.find (f, g) m = Some fg.
proof: Proof. intros. destruct (N.eq_dec x f). - destruct (N.eq_dec y g). + destruct (N.eq_dec z fg). * subst; left; intuition. * contradiction n. rewrite F.add_eq_o in H. ** inversion_clear H. reflexivity. ** simpl; intuition. + rewrite F.add_neq_o in H; intuition. - rewrite F.add_neq_o in H; intuition. Defined.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor