proposition: Lemma composition_left {x y z : object} {f : morphism y z} {g : morphism x y} {fg : arrow M} : composite M (mor_arr f) (mor_arr g) fg -> composite M (obj_arr z) (mor_arr f) (mor_arr f) -> composite M (obj_arr z) fg fg.
proof: Proof. intros. destruct z, obj_id0 as [c c0], f, g; simpl in *. specialize (c0 _ (composite_defined M H0)); clear H0. destruct (composite_correct M c0 H). spose (fst (composition_law M c0 H _) e) as X. unfold composite, arrow in *. rewrite X, <- H, <- e; reflexivity. Qed.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor