proposition: Lemma is_finite_cat_opp : forall a, is_finite_cat a -> is_finite_cat (opp a).
proof: Proof. ir. uhg; dj. ap opp_axioms. uh H; ee; am. assert (objects (opp a) = objects a). ap extensionality; uhg; ir. assert (ob (opp a) x). app is_ob_ob. ap ob_is_ob. wr ob_opp. am. assert (ob a x). ap is_ob_ob. wrr axioms_opp. am. ap ob_is_ob. rww ob_opp. rw H1. uh H; ee; am. ap finite_invariant. sh (morphisms a). ee. ap opp_morphisms_isomorphic. wrr axioms_opp. uh H; ee. am. Qed.
imports: Arith cat_examples cardinal fc_limits