proposition: Lemma limit_preservation_invariance : is_limit (cone_pushdown f a).
proof: Proof. ir. ap (cone_to_limit_invertible_is_limit (a:= (cone_pushdown f a)) (b:=(cone_pushdown f b))). am. app is_cone_cone_pushdown. cp K0; lu. rw K3; uf cone_target; rww K2. rw socle_cone_pushdown. rw socle_cone_pushdown. rww K2. wr fmor_cone_to_limit. rw cone_target_cone_pushdown. ap invertible_fmor_ctl. am. cp K0; lu. am. am. am. am. Qed.
imports: Arith nat_trans