proposition: Lemma composition_associative {x y z w : object} (f : morphism z w) (g : morphism y z) (h : morphism x y) : composition f (composition g h) ≈ composition (composition f g) h.
proof: Proof. destruct f, g, h; simpl. repeat destruct (composite_correct _ _ _); simpl in *. spose (fst (composition_law M e1 e x3) e2) as X1. unfold composite, arrow in *. rewrite e0 in X1. inversion_clear X1. reflexivity. Qed.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor