proposition: Lemma socle_newcone : forall u, mor a u -> socle (newcone u) = pointf (target u).
proof: Proof. ir. uf newcone. rw socle_cone_transform. rw target_htrans_right. rw target_point_trans. tv. Qed.
imports: Arith colimits functor_cat