Search code examples
coq

Unifying types of identical meanings

I have this goal:

forall n m : nat, S n > m -> n >= m

The gt_S lemmata would be applicable to prove it but Coq won't unify the two types.

gt_S: forall n m : nat, S n > m -> n > m \/ m = n

What would be the simplest solution here (excluding lia)?

Solution

  • In this case you can use forward reasoning by using apply .. in rather than plain apply.

    Goal forall n m : nat, S n > m -> n >= m.
Proof.
  intros n m h.
  apply gt_S in h.

    After which hypothesis h is now h : n > m \/ m = n. Hopefully you should be able to progress from there.