proposition: Lemma cone_compose_cone_pushdown_fmor_cone_to_limit : cone_compose (cone_pushdown f b) (fmor f (cone_to_limit a b)) = cone_pushdown f a.
proof: Proof. assert (lem0 : is_cone b). cp K1. uh H; ee. lu. assert (lem1 : a = cone_compose b (cone_to_limit a b)). rww cone_compose_cone_to_limit. transitivity (cone_pushdown f (cone_compose b (cone_to_limit a b))). assert (cone_pushdown f (cone_compose b (cone_to_limit a b)) = cone_compose (cone_pushdown f b) (fmor f (cone_to_limit a b))). rw cone_pushdown_cone_compose. reflexivity. am. am. am. app mor_cone_to_limit. rww target_cone_to_limit. rw H. reflexivity. assert (cone_compose b (cone_to_limit a b) = a). rw cone_compose_cone_to_limit. tv. am. am. am. rw H. reflexivity. Qed.
imports: Arith nat_trans