English
If h1 ensures that oadd e1 n1 a1 is NFBelow b1, then for any o2, b2 with NFBelow, the product oadd e1 n1 a1 * o2 is NFBelow repr e1 + b2.
Русский
Если для некоторого e1,n1,a1 выполнено, что oadd e1 n1 a1 находится ниже NF относительно b1, то для любого o2,b2 с NFBelow выполняется: (oadd e1 n1 a1) * o2 ниже (repr e1 + b2).
LaTeX
$$$\forall {e_1\, n_1\, a_1\, b_1} (h_1 : NFBelow (oadd e_1 n_1 a_1) b_1),\; \forall {o_2\, b_2} (h_2 : NFBelow o_2 b_2),\; NFBelow (oadd e_1 n_1 a_1 * o_2) (\mathrm{repr}(e_1) + b_2).$$$
Lean4
theorem oadd_mul_nfBelow {e₁ n₁ a₁ b₁} (h₁ : NFBelow (oadd e₁ n₁ a₁) b₁) :
∀ {o₂ b₂}, NFBelow o₂ b₂ → NFBelow (oadd e₁ n₁ a₁ * o₂) (repr e₁ + b₂)
| 0, _, _ => NFBelow.zero
| oadd e₂ n₂ a₂, b₂, h₂ => by
have IH := oadd_mul_nfBelow h₁ h₂.snd
by_cases e0 : e₂ = 0 <;> simp only [e0, oadd_mul, ↓reduceIte]
· apply NFBelow.oadd h₁.fst h₁.snd
simpa using (add_lt_add_iff_left (repr e₁)).2 (lt_of_le_of_lt (Ordinal.zero_le _) h₂.lt)
· haveI := h₁.fst
haveI := h₂.fst
apply NFBelow.oadd
· infer_instance
· rwa [repr_add]
· rw [repr_add, add_lt_add_iff_left]
exact h₂.lt
