NNG le_total

Stream: new members

[Thomas Laraia]

I am looking for approaches to this problem and creating hypotheses that I can work with, specifically cases since this seems like a viable route.
This following leads to a statement that I cannot prove.

induction b with d hd,
right,
exact zero_le a,
cases hd,
left,
apply le_succ,
exact hd,

I also found this archive discussing it but found it difficult to continue with only beginner understanding.

classical,
by_cases a ≤ b,
left,
exact h,

Is there a good way to establish cases or induction to work with in this specific case?

[Johan Commelin]

@Thomas Laraia could you please link to the exact level of NNG that you are working on?

[Thomas Laraia]

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=10&level=9

[Johan Commelin]

@Thomas Laraia You can use le_iff_exists_add

[Johan Commelin]

rw le_iff_exists_add at hd, allows you to continue your proof.