English
For o1,o2 with NF, repr(o1 - o2) = repr(o1) - repr(o2).
Русский
Для o1,o2 с NF, repr(o1 - o2) = repr(o1) - repr(o2).
LaTeX
$$$\forall o_1,o_2 : ONote\,[o_1.NF][o_2.NF],\; repr(o_1 - o_2) = repr(o_1) - repr(o_2)$$$
Lean4
@[simp]
theorem repr_sub : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ - o₂) = repr o₁ - repr o₂
| 0, o, _, h₂ => by cases o <;> exact (Ordinal.zero_sub _).symm
| oadd _ _ _, 0, _, _ => (Ordinal.sub_zero _).symm
| oadd e₁ n₁ a₁, oadd e₂ n₂ a₂, h₁, h₂ => by
haveI := h₁.snd; haveI := h₂.snd; have h' := repr_sub a₁ a₂
conv_lhs at h' => dsimp [HSub.hSub, Sub.sub, sub]
conv_lhs => dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]
have ee := @cmp_compares _ _ h₁.fst h₂.fst
cases h : cmp e₁ e₂ <;> simp only [h] at ee
· rw [Ordinal.sub_eq_zero_iff_le.2]
· rfl
exact le_of_lt (oadd_lt_oadd_1 h₁ ee)
· change e₁ = e₂ at ee
subst e₂
dsimp only
cases mn : (n₁ : ℕ) - n₂ <;> dsimp only
· by_cases en : n₁ = n₂
· simpa [en]
· simp only [en, ite_false]
exact
(Ordinal.sub_eq_zero_iff_le.2 <|
le_of_lt <| oadd_lt_oadd_2 h₁ <| lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm
· simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, Nat.cast_add, Nat.cast_one, add_one_eq_succ]
rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm, Nat.cast_add, mul_add,
add_assoc, add_sub_add_cancel]
refine (Ordinal.sub_eq_of_add_eq <| add_absorp h₂.snd'.repr_lt <| le_trans ?_ (le_add_right _ _)).symm
exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)
· exact (Ordinal.sub_eq_of_add_eq <| add_absorp (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm
