proposition: Lemma comp_fmor : forall f u v, axioms f -> mor (source f) u -> mor (source f) v -> source u = target v -> comp (target f) (fmor f u) (fmor f v) = fmor f (comp (source f) u v).
proof: Proof. ir. uh H; ee. au. Qed.
imports: Arith category