proposition: Lemma cocone_pushdown_are_inverse_invol : forall a f g, is_cocone a -> are_finverse f g -> source f = cocone_target a -> cocone_pushdown g (cocone_pushdown f a) = a.
proof: Proof. ir. ap cocone_extensionality. ap is_cocone_cocone_pushdown. ap is_cocone_cocone_pushdown. am. uh H0; ee; am. am. uh H0; ee; am. rw cocone_target_cocone_pushdown. uh H0; ee; am. am. rw vertex_cocone_pushdown. rw vertex_cocone_pushdown. wr fob_fcompose. uh H0; ee. rw H6. rw fob_fidentity. tv. rw H1. ap ob_vertex. am. uh H0; ee; am. uh H0; ee; am. uh H0; ee; am. rw H1. ap ob_vertex. am. rw cosocle_cocone_pushdown. rw cosocle_cocone_pushdown. wr fcompose_assoc. uh H0; ee. rw H6. rw left_fidentity. tv. ap cosocle_axioms. am. am. uh H0; ee; am. uh H0; ee; am. ap cosocle_axioms. am. uh H0; ee; am. am. ir. rwi cocone_source_cocone_pushdown H2. rwi cocone_source_cocone_pushdown H2. uh H0; ee. rw coedge_cocone_pushdown. rw coedge_cocone_pushdown. wr fmor_fcompose. rw H7. rw fmor_fidentity. tv. rw H1. ap mor_coedge. am. am. am. am. am. rw H1. ap mor_coedge. am. am. am. am. rw cocone_source_cocone_pushdown. am. ap is_cocone_cocone_pushdown. am. am. am. Qed.
imports: Arith limits