proposition: Lemma cone_to_limit_invertible_is_limit : forall a b, is_limit b -> is_cone a -> socle a = socle b -> invertible (cone_target b) (cone_to_limit a b) -> is_limit a.
proof: Proof. ir. assert (a = cone_compose b (cone_to_limit a b)). rw cone_compose_cone_to_limit. tv. am. am. am. rw H3. ap is_limit_cone_compose. am. uhg; ee. uh H; ee. uh H; ee; am. app mor_cone_to_limit. rww target_cone_to_limit. lu. Qed.
imports: Arith nat_trans