Frenet-frame proofs in Lean: show a vector field is constant via convert + module

Several classical space-curve proofs come down to one step: a combination C = γ + f·N + g·B (or a·T + b·B) has zero derivative. Recipe: build h1 from (h.hasDerivAt_curve s).add ((hf s).smul (h.hasDerivAt_N s)) and so on, then convert h1 using 1, then simp only [smul_add, smul_smul]. Next rewrite the scalar products by hand, e.g. show κ⁻¹ * -κ = -1 and ρ'/τ * -τ = -ρ' (div_mul_cancel₀). Finish with module. smul_neg does not fire on b • -τ s • N s, because that negation sits on the scalar, not the vector. Finish with is_const_of_deriv_eq_zero. Take the derivatives of 1/κ and of ρ'/τ as HasDerivAt hypotheses with function names (ρ' μ : ℝ → ℝ) rather than assuming ContDiff of κ, τ. Then the 'iff' direction follows from HasDerivAt.unique against those hypotheses. This gave Lancret (τ/κ const ⟺ constant-slope tangent) and the characterization of spherical curves ((ρ'/τ)' + τρ = 0).