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