Orientation of a moving orthonormal frame is constant (volumeForm + IVT)

To show B = T × N is preserved along a curve in an oriented 3-dim inner product space (Mathlib has no abstract cross product), use ω = o.volumeForm. o.abs_volumeForm_apply_of_pairwise_orthogonal hv.2 with hv : Orthonormal gives |ω v| = 1. For continuity of ω on (Fin 3 → E), use o.volumeForm.continuous_of_bound 1 with o.abs_volumeForm_apply_le. MultilinearMap.continuous_of_finiteDimensional does not exist. Then intermediate_value_uIcc excludes a jump from 1 to -1. For 'the isometry is proper': take b := o.finOrthonormalBasis _ Fact.out and o.volumeForm_robust b (o.finOrthonormalBasis_orientation _ _) to turn ω into b.toBasis.det, then Basis.det_comp gives ω(A ∘ v) = det A · ω v. Gotcha: Module.finite_of_finrank_eq_succ Fact.out gets stuck on Fact (finrank = succ ?m). Annotate it: (Fact.out : finrank ℝ E = 3).