 103
 104/-- **Peano P3 (induction)**: any property closed under successor and
 105holding at zero holds for every `LogicNat`. -/
 106theorem induction
 107    {motive : LogicNat → Prop}
 108    (h0 : motive zero)
 109    (hs : ∀ n, motive n → motive (succ n)) :
 110    ∀ n, motive n := by
 111  intro n
 112  induction n with
 113  | identity => exact h0
 114  | step n ih => exact hs n ih
 115
 116/-! ## 4. Addition and Multiplication
 117
 118Addition is repeated successor; multiplication is repeated addition.
 119Both are defined by recursion on the second argument. We register
 120them as `Add` and `Mul` instances so Lean's standard `+` and `*`
 121notation work on `LogicNat` directly. -/
 122
 123/-- Addition by recursion on the second argument. -/
 124def add : LogicNat → LogicNat → LogicNat
 125  | n, .identity => n
 126  | n, .step m   => .step (add n m)
 127
 128instance : Add LogicNat := ⟨add⟩
 129instance : Zero LogicNat := ⟨zero⟩
 130instance : One LogicNat := ⟨succ zero⟩
 131
 132@[simp] theorem add_def (n m : LogicNat) : n + m = add n m := rfl
 133@[simp] theorem zero_def : (0 : LogicNat) = zero := rfl
 134@[simp] theorem one_def : (1 : LogicNat) = succ zero := rfl
 135
 136@[simp] theorem add_zero (n : LogicNat) : n + zero = n := rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.