proposition: Lemma dotted_cone_compose : forall u a, cone_composable a u -> has_limit (socle a) -> dotted (cone_compose a u) = comp (cone_target a) (dotted a) u.
proof: Proof. ir. uf dotted. rw cone_to_limit_cone_compose. rw socle_cone_compose. rw cone_target_limit. rw target_socle. reflexivity. am. app is_limit_limit. rw socle_cone_compose. am. am. rw socle_limit. rw socle_cone_compose. tv. rww socle_cone_compose. Qed.
imports: Arith nat_trans