proposition: Lemma cone_composable_dotted : forall a, is_cone a -> has_limit (socle a) -> cone_composable (limit (socle a)) (dotted a).
proof: Proof. ir. uf cone_composable. ee. ap is_limit_is_cone. app is_limit_limit. rww cone_target_limit. rw target_socle. app mor_dotted. rww target_dotted. Qed.
imports: Arith nat_trans