proposition: Lemma is_cone_fiprod_cone : forall a u v y1 y2, fiprod_hypothesis a u v y1 y2 -> is_cone (fiprod_cone a u v y1 y2).
proof: Proof. ir. uhg; ee. uf fiprod_cone. ap cone_like_cone_create. rw edge_nt_fiprod_cone. ap vee_nt_axioms. app fiprod_vee_nt_hypothesis. rw cone_target_fiprod_cone. rw vertex_fiprod_cone. uh H; ee. rww ob_source. rw edge_nt_fiprod_cone. rw source_vee_nt. rw cone_source_fiprod_cone. rw cone_target_fiprod_cone. rw vertex_fiprod_cone. sy; rw constant_functor_vee_functor. uh H; ee. rww H4. tv. uh H; ee. rww ob_source. Qed.
imports: Arith colimits little_cat fc_limits cardinal