proposition: Lemma commutativity : forall c u, mor (cone_source c) u -> is_cone c -> comp (cone_target c) (fmor (socle c) u) (edge c (source u)) = edge c (target u).
proof: Proof. ir. uh H0; ee. uf edge. assert (cone_target c = otarget (edge_nt c)). rww otarget_edge_nt. assert (socle c = target (edge_nt c)). rww target_edge_nt. assert (lem1: forall y, ntrans (edge_nt c) y = edge c y). ir. tv. rw H4; rw H5. wr carre. rw source_edge_nt. rw fmor_constant_functor. rw right_id. tv. wr H4; am. wr H4. change (mor (cone_target c) (edge c (target u))). app mor_edge. rww ob_target. uhg; ee; am. rw lem1. rww source_edge. rww ob_target. uhg; ee; am. rww otarget_edge_nt. am. uhg; ee; am. am. rww osource_edge_nt. uhg; ee; am. Qed.
imports: Arith nat_trans