proposition: Lemma fmor_cone_to_limit : fmor f (cone_to_limit a b) = cone_to_limit (cone_pushdown f a) (cone_pushdown f b).
proof: Proof. cp K4. uh H; ee. uh H; ee. assert (is_cone b). cp K1. uh H2; ee; lu. assert (is_versal b). cp K1; lu. ap H1. uhg; ee. app is_cone_cone_pushdown. rww cone_target_cone_pushdown. app mor_fmor. rw K3. app mor_cone_to_limit. rww target_fmor. rww vertex_cone_pushdown. rww target_cone_to_limit. rw K3; app mor_cone_to_limit. uhg; ee. app is_cone_cone_pushdown. rww cone_target_cone_pushdown. ap mor_cone_to_limit. ap is_cone_cone_pushdown. am. am. rw K3. uf cone_target. rww K2. am. rww socle_cone_pushdown. rw socle_cone_pushdown. rww K2. rww cone_target_cone_pushdown. rw target_cone_to_limit. tv. app is_cone_cone_pushdown. rw K3; uf cone_target; rww K2. am. rww socle_cone_pushdown. rw socle_cone_pushdown. rww K2. rw cone_compose_cone_pushdown_fmor_cone_to_limit. sy; rw cone_compose_cone_to_limit. tv. app is_cone_cone_pushdown. rw K3; uf cone_target; rww K2. am. rw socle_cone_pushdown. rw socle_cone_pushdown. rww K2. Qed.
imports: Arith nat_trans