proposition: Lemma cone_to_limit_pr : forall a b, is_cone a -> is_limit b -> socle a = socle b -> (cone_composable b (cone_to_limit a b) & cone_compose b (cone_to_limit a b) = a).
proof: Proof. ir. uh H0; ee. uh H2; ee. util (H3 a). am. am. cp (choose_pr H4). cbv beta in H5. ee. am. uh H2; ee. util (H3 a). am. am. cp (choose_pr H4). cbv beta in H5. ee. am. Qed.
imports: Arith nat_trans