proposition: Lemma cone_pushdown_are_inverse_invol : forall a f g, is_cone a -> are_finverse f g -> source f = cone_target a -> cone_pushdown g (cone_pushdown f a) = a.
proof: Proof. ir. ap cone_extensionality. ap is_cone_cone_pushdown. ap is_cone_cone_pushdown. am. uh H0; ee; am. am. uh H0; ee; am. rw cone_target_cone_pushdown. uh H0; ee; am. am. rw vertex_cone_pushdown. rw vertex_cone_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 socle_cone_pushdown. rw socle_cone_pushdown. wr fcompose_assoc. uh H0; ee. rw H6. rw left_fidentity. tv. ap socle_axioms. am. am. uh H0; ee; am. uh H0; ee; am. ap socle_axioms. am. uh H0; ee; am. am. ir. rwi cone_source_cone_pushdown H2. rwi cone_source_cone_pushdown H2. uh H0; ee. rw edge_cone_pushdown. rw edge_cone_pushdown. wr fmor_fcompose. rw H7. rw fmor_fidentity. tv. rw H1. ap mor_edge. am. am. am. am. am. rw H1. ap mor_edge. am. am. am. am. rw cone_source_cone_pushdown. am. ap is_cone_cone_pushdown. am. am. am. Qed.
imports: Arith nat_trans