proposition: Lemma source_cone_to_limit : forall a b, is_cone a -> is_limit b -> socle a = socle b -> source (cone_to_limit a b) = vertex a.
proof: Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. transitivity (vertex (cone_compose b (cone_to_limit a b))). rw vertex_cone_compose. tv. rw H3. tv. Qed.
imports: Arith nat_trans