theorem Bounding.Rx_norm_one (α : ℝ) : ‖RxL α‖ = 1

theorem Bounding.Ry_norm_one (α : ℝ) : ‖RyL α‖ = 1

theorem Bounding.Rz_norm_one (α : ℝ) : ‖RzL α‖ = 1

theorem Bounding.rotR_norm_one (α : ℝ) :
  ‖rotR α‖ = 1

theorem Bounding.rotM_norm_one (θ φ : ℝ) :
  ‖rotM θ φ‖ = 1

theorem Bounding.rotR'_norm_one (α : ℝ) :
  ‖rotR' α‖ = 1

theorem Bounding.rotMθ_norm_le_one (θ φ : ℝ) :
  ‖rotMθ θ φ‖ ≤ 1

theorem Bounding.rotMφ_norm_le_one (θ φ : ℝ) :
  ‖rotMφ θ φ‖ ≤ 1

theorem Bounding.norm_rotR_sub_rotR_lt
  {ε α α_ : ℝ} (hε : 0 < ε)
  (hα : |α - α_| ≤ ε) :
  ‖rotR α - rotR α_‖ < ε

theorem Bounding.norm_RxL_sub_RxL_eq {α α_ : ℝ} :
  ‖RxL α - RxL α_‖ = ‖rotR α - rotR α_‖

theorem Bounding.norm_RyL_sub_RyL_eq {α α_ : ℝ} :
  ‖RyL α - RyL α_‖ = ‖rotR α - rotR α_‖

theorem Bounding.norm_RzL_sub_RzL_eq {α α_ : ℝ} :
  ‖RzL α - RzL α_‖ = ‖rotR α - rotR α_‖

theorem Bounding.lemma12 {d d' : Fin 3} {α β : ℝ}
  (d_ne_d' : d ≠ d') :
  ‖(rot3 d) α ∘SL (rot3 d') β - 1‖ ≤
    √(α ^ 2 + β ^ 2)

theorem Bounding.lemma12_equality_iff
  {d d' : Fin 3} {α β : ℝ}
  (d_ne_d' : d ≠ d') :
  ‖(rot3 d) α ∘SL (rot3 d') β - 1‖ =
      √(α ^ 2 + β ^ 2) ↔
    α = 0 ∧ β = 0

theorem Bounding.norm_M_sub_lt {ε θ θ_ φ φ_ : ℝ}
  (hε : 0 < ε) (hθ : |θ - θ_| ≤ ε)
  (hφ : |φ - φ_| ≤ ε) :
  ‖rotM θ φ - rotM θ_ φ_‖ < √2 * ε

theorem Bounding.norm_X_sub_lt {ε θ θ_ φ φ_ : ℝ}
  (hε : 0 < ε) (hθ : |θ - θ_| ≤ ε)
  (hφ : |φ - φ_| ≤ ε) :
  ‖vecX θ φ - vecX θ_ φ_‖ < √2 * ε

theorem Bounding.XPgt0 {P : Euc(3)}
  {ε θ θ_ φ φ_ : ℝ} (hP : ‖P‖ ≤ 1)
  (hε : 0 < ε) (hθ : |θ - θ_| ≤ ε)
  (hφ : |φ - φ_| ≤ ε)
  (hX : √2 * ε < ⟪vecX θ_ φ_, P⟫) :
  0 < ⟪vecX θ φ, P⟫

theorem Bounding.norm_M_apply_gt
  {ε r θ θ_ φ φ_ : ℝ} {P : Euc(3)}
  (hP : ‖P‖ ≤ 1) (hε : 0 < ε)
  (hθ : |θ - θ_| ≤ ε) (hφ : |φ - φ_| ≤ ε)
  (hM : r + √2 * ε < ‖(rotM θ_ φ_) P‖) :
  r < ‖(rotM θ φ) P‖

theorem Bounding.norm_RM_sub_RM_le
  {ε θ θ_ φ φ_ α α_ : ℝ} (hε : 0 < ε)
  (hθ : |θ - θ_| ≤ ε) (hφ : |φ - φ_| ≤ ε)
  (hα : |α - α_| ≤ ε) :
  ‖rotprojRM θ φ α - rotprojRM θ_ φ_ α_‖ <
    √5 * ε