proposition: Lemma cone_compose_fiprod_cone : forall a u v y1 y2 z, fiprod_hypothesis a u v y1 y2 -> mor a z -> source y1 = target z -> cone_compose (fiprod_cone a u v y1 y2) z = fiprod_cone a u v (comp a y1 z) (comp a y2 z).
proof: Proof. ir. assert (lem1: fiprod_hypothesis a u v (comp a y1 z) (comp a y2 z)). uh H; uhg; ee. am. rww mor_comp. rww mor_comp. wrr H6. rww target_comp. rww target_comp. wrr H6. rww source_comp. rww source_comp. wrr H6. wr assoc. rw H7. rww assoc. uh H; ee; am. wrr H6. uh H; ee; am. am. am. am. am. tv. assert (lem2 : cone_composable (fiprod_cone a u v y1 y2) z). uhg; ee. app is_cone_fiprod_cone. rww cone_target_fiprod_cone. rww vertex_fiprod_cone. sy; am. ap fimaps_extensionality. rww is_cone_cone_compose. app is_cone_fiprod_cone. rw cone_source_cone_compose. rww cone_source_fiprod_cone. rw socle_cone_compose. rww socle_fiprod_cone. rww socle_fiprod_cone. rww fimap1_cone_compose. rww cone_target_fiprod_cone. rww fimap1_fiprod_cone. rww fimap1_fiprod_cone. app is_cone_fiprod_cone. rww cone_source_fiprod_cone. rww fimap2_cone_compose. rww cone_target_fiprod_cone. rww fimap2_fiprod_cone. rww fimap2_fiprod_cone. app is_cone_fiprod_cone. rww cone_source_fiprod_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal