I can write b<a and if b<a so their Succ also keep the relation? Secondly , want to remove S from both sides of H2 so that it become ~ a < S b. Then apply (<=)relation so that it become ~ a <= b.

```
a, b : nat
H1 : (a <=? b) = false
goal:S b < S a
H2: ~ S a < S (S b)
goal: (a <=? b) = false.
```

`Nat.leb_gt`

should help. Also: https://coq.inria.fr/refman/addendum/micromega.html (`lia`

tactic)

Very good reference.

Last updated: Sep 26 2023 at 13:01 UTC