def Fixpoint.Examples.EvenAux (p : ℕ → Prop) (n : ℕ) : Prop

Equations

• Fixpoint.Examples.EvenAux p n = (n = 0 ∨ ∃ (k : ℕ), p k ∧ k + 2 = n)

def Fixpoint.Examples.Even' : ℕ → Prop

Equations

• Fixpoint.Examples.Even' = Fixpoint.IndPred Fixpoint.Examples.EvenAux

@[simp]

theorem Fixpoint.Examples.monotone_evenAux : Monotone EvenAux

@[simp]

theorem Fixpoint.Examples.even'_zero : Even' 0

theorem Fixpoint.Examples.even'_add_two {n : ℕ} (h : Even' n) : Even' (n + 2)

theorem Fixpoint.Examples.even'_cases {n : ℕ} (h : Even' n) : n = 0 ∨ ∃ (k : ℕ), Even' k ∧ k + 2 = n

theorem Fixpoint.Examples.even'_ind {p : ℕ → Prop} {n : ℕ} (h₁ : Even' n) (h₂ : p 0) (h₃ : ∀ (n : ℕ), Even' n → p n → p (n + 2)) : p n

theorem Fixpoint.Examples.even'_eq_even : Even' = Even