proposition: Lemma invertible_cone_to_limit : forall a b c, is_limit a -> is_limit b -> socle a = socle b -> cone_target a = c -> invertible c (cone_to_limit a b).
proof: Proof. ir. uhg. sh (cone_to_limit b a). app are_inverse_cone_to_limit. Qed.
imports: Arith nat_trans