Commit 2026-07-25 09:21 c8830a1d

feat(Manifold/Instances/Icc): golf smoothness proof using immersions (#29077) Prove that the inclusion of an interval into the real numbers is a smooth embedding, and use this to golf the proof that this inclusion is smooth. While at it, rename the smoothness lemmas after the coercion Subtype.val they are using, as mandated by the naming convention.