proposition: Lemma invertible_dotted_is_limit : forall a, is_cone a -> has_limit (socle a) -> invertible (cone_target a) (dotted a) -> is_limit a.
proof: Proof. ir. assert (a = cone_compose (limit (socle a)) (dotted a)). rww cone_compose_dotted. rw H2. app is_limit_cone_compose. app is_limit_limit. app cone_composable_dotted. rw cone_target_limit. rw target_socle. am. am. Qed.
imports: Arith nat_trans