nf_opowAux — Mathlib

English

For e, a0, a in ONote, if e, a0, a are in normal form, then for all k, m ∈ Nat, NF(opowAux(e, a0, a, k, m)).

Русский

Для e, a0, a ∈ ONote, если они в нормальной форме, то для всех k, m ∈ Nat выполняется NF(opowAux(e, a0, a, k, m)).

LaTeX

$$$\\forall k,m:\\, \\operatorname{NF}(\\operatorname{opowAux}(e,a_0,a,k,m))$$$

Lean4

instance nf_opowAux (e a0 a) [NF e] [NF a0] [NF a] : ∀ k m, NF (opowAux e a0 a k m) :=
  by
  intro k m
  unfold opowAux
  cases m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      haveI := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

Похожие утверждения