proposition: Lemma is_limit_invertible_dotted : forall a, is_limit a -> invertible (cone_target a) (dotted a).
proof: Proof. ir. uf dotted. assert (has_limit (socle a)). uhg. sh a. uhg; ee. am. tv. ap invertible_cone_to_limit. am. ap is_limit_limit. am. rww socle_limit. tv. Qed.
imports: Arith nat_trans