English
Let o be an ONote in normal form. If its split is o' paired with a natural number m, then o' is in normal form and the representation of o equals the sum of the representation of o' and m, i.e., repr(o) = repr(o') + m.
Русский
Пусть o — ONote в нормальной форме. Если разбиение o даёт пару (o', m) с m ∈ Nat, то o' имеет NF и представление repr(o) равно repr(o') + m, то есть repr(o) = repr(o') + m.
LaTeX
$$$\\forall o o' m\\,[NF\\ o]\\;\\big( split\\ o = (o', m) \\big) \\Rightarrow (NF\\ o' \\land \\operatorname{repr} o = \\operatorname{repr} o' + m)$$$
Lean4
theorem nf_repr_split {o o' m} [NF o] (h : split o = (o', m)) : NF o' ∧ repr o = repr o' + m :=
by
rcases e : split' o with ⟨a, n⟩
obtain ⟨s₁, s₂⟩ := nf_repr_split' e
rw [split_eq_scale_split' e] at h
injection h; substs o' n
simp only [repr_scale, repr_one, Nat.cast_one, opow_one, ← s₂, and_true]
infer_instance
