have : x * y = g := by
  apply eqg; native_decide
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this : z⁻¹ = g
⊢ False
g : P
left✝ : (fun x => FreeModule.coordinates x α ≠ 0) g
eqg : ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
this✝ : z⁻¹ = g
this : x * y = g
⊢ False