proposition: Lemma subcategory_axioms : forall a obp morp, subcategory_property a obp morp -> Category.axioms (subcategory a obp morp).
proof: Proof. ir. cp H. uh H0; ee. uf subcategory. ap Category.create_axioms. uhg; ee; ir. ap iff_eq; ir. Ztac. assert (ob a x). app is_ob_ob. uhg; ee. Ztac. ap Z_inc. ap mor_is_mor. app mor_id. app H2. rww source_id. rww target_id. uh H5; ee. ap Z_inc. pose (Z_all H5). ee. am. pose (Z_all H5); ee. am. ap iff_eq; ir. Ztac. assert (mor a u). ap is_mor_mor. am. am. uhg; ee. app Z_inc. app Z_inc. ap ob_is_ob. rww ob_source. app H3. ap Z_inc. ap ob_is_ob. rww ob_target. app H4. rww right_id. rww ob_source. rww left_id. rww ob_target. apply mor_arrow_like with a. am. uh H5; ee. pose (Z_all H5). ee. Ztac. Ztac. clear H6. Ztac. clear H5. assert (mor a u). app is_mor_mor. assert (mor a v). app is_mor_mor. uhg; ee. Ztac. Ztac. am. Ztac. ap mor_is_mor. rww mor_comp. rww source_comp. rww target_comp. assert (mor a u). pose (Z_all H5); ee; app is_mor_mor. assert (mor a v). pose (Z_all H6); ee; app is_mor_mor. assert (mor a w). pose (Z_all H7); ee; app is_mor_mor. rww assoc. Qed.
imports: Arith ordinal nat_trans