more complicated case-splits

Stream: general

[Jakub Kądziołka]

n : \N. What's the best way to separately consider the cases n = 0, n = 1, and n \ge 2?

[Yakov Pechersky]

rcases n with _|_|n,

[Jakub Kądziołka]

What if I want to keep n \ge 2 as an assumption instead of dealing with n.succ.succ?

[Eric Rodriguez]

i made docs#nat.two_le_iff recently, although it's a bit clunky

[Eric Rodriguez]

another clunky way is lt_trichotomy 1 n, taking advantage that 1 < n is defeq to 2 ≤ n, but also not perfeect

[Riccardo Brasca]

You can just set m := n.succ.succ and prove that 2 ≤ m (this should be a one liner)

[Yakov Pechersky]

cases le_or_lt 2 n with h h

[Kevin Buzzard]

rcases lt_trichotomy 1 n with ((h2 : 2 ≤ n) | rfl | - | ⟨-, ⟨-⟩⟩)

[Eric Rodriguez]

Kevin Buzzard said:

rcases lt_trichotomy 1 n with ((h2 : 2 ≤ n) | rfl | - | ⟨-, ⟨-⟩⟩)

This looks about as readable as Malbolge

[Mario Carneiro]

You must not read coq code often

[Eric Rodriguez]

Felt like I didn't wanna cause another theorem prover war in the middle of a conference :b