Showing falsity in a 'le' exercise from 'IndProp'

Using Coq
1

Hello!

I am stuck in the following problem. I’ve made multiple attempts at it, and below is one which I think should work. But, I am unable to prove the very apparent falsity of the statement in the goal using the context.
image

This is how the goal monitor looks:
image

I’d appreciate any help/hints on this. Thanks so much!

2

Proving the falsity of the goal accomplishes nothing useful from a logical standpoint. You need to either:

  • Prove the falsity of a hypothesis (thereby deriving a contradiction), or
  • Prove the truthity of the goal.
3

When you’re stuck in a proof for more than five minutes: Instead of “what tactic should I use?” better ask yourself “what am I trying to do?”
Explain—in natural language—your proof strategy. Here you have a hypothesis S n <= S m, which is defined inductively. What are all the possible ways to construct this hypothesis? How to perform case analysis on the possibilities? What hypotheses do you get when performing the case analyses?

1 Like