Proof by cases on Nat

Stream: new members

[Jesse Slater]

I want to prove something by cases on a Nat n. the cases should be n = 0, n = 1, n > 1. How do I do this?

[Riccardo Brasca]

rcases n with (rfl | rfl | n) should produce three goals, one for 0, one for 1 and one for n.succ.succ. Proving that 1 < n.succ.succ should be easy.

[Riccardo Brasca]

You can also use a preliminary result (that is maybe in mathlib, I didn't search) to literally obtain the three cases.

lemma foo (n : ℕ) : n = 0 ∨ n = 1 ∨ 1 < n :=
by rcases n with (rfl | rfl | n); simp

lemma bar (n : ℕ) : true :=
begin
  rcases foo n with (rfl | rfl | n),
  ...
end

[Jesse Slater]

Thanks!