theorem
Garrett.wittCancellation_independent
{k : Type u_1}
[Field k]
[NeZero 2]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
(B : LinearMap.BilinForm k V)
(hSym : ∀ (x y : V), (B x) y = (B y) x)
(hNd : B.orthogonal ⊤ = ⊥)
:
Witt cancellation holds for any nondegenerate symmetric bilinear form on a finite-dimensional space (in characteristic not two).