## Stream: general

### Topic: more complicated case-splits

#### Jakub Kądziołka (Mar 03 2022 at 19:43):

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

#### Yakov Pechersky (Mar 03 2022 at 19:46):

rcases n with _|_|n,


#### Jakub Kądziołka (Mar 03 2022 at 19:47):

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

#### Eric Rodriguez (Mar 03 2022 at 19:48):

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

#### Eric Rodriguez (Mar 03 2022 at 19:49):

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

#### Riccardo Brasca (Mar 03 2022 at 19:56):

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

#### Yakov Pechersky (Mar 03 2022 at 20:03):

cases le_or_lt 2 n with h h

#### Kevin Buzzard (Mar 03 2022 at 22:22):

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

#### Eric Rodriguez (Mar 03 2022 at 22:33):

Kevin Buzzard said:

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

This looks about as readable as Malbolge

#### Mario Carneiro (Mar 03 2022 at 22:34):

You must not read coq code often

#### Eric Rodriguez (Mar 03 2022 at 22:36):

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

Last updated: Dec 20 2023 at 11:08 UTC