simp [models_def, omegaOneAxiom, length_defined.df.iff, Exponential.defined.df.iff, sq, ←le_iff_lt_succ]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ M ⊧ₘ omegaOneAxiom ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ ^ 2) y
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y