proposition: Lemma cone_source_cone_transform : forall u c, cone_transformable u c -> cone_source (cone_transform u c) = cone_source c.
proof: Proof. ir. uf cone_source. rw socle_cone_transform. uh H; ee. rww source_target. uf osource; rww H1. Qed.
imports: Arith nat_trans