proposition: Lemma is_cofiprod_cofiprod : forall a u v, has_cofiprod a u v -> is_cofiprod a u v (cofipr1 a u v) (cofipr2 a u v).
proof: Proof. ir. assert (Category.axioms a). uh H; ee. uh H; ee. uh H; ee; am. uhg; ee; try am. uf cofipr1; uf cofipr2. rw flip_flip. rw flip_flip. ap is_fiprod_fiprod. uh H; ee. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal