Stream: Coq users

Topic: Relation with Successor

view this post on Zulip sara lee (Sep 12 2021 at 04:43):

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.

view this post on Zulip Karl Palmskog (Sep 12 2021 at 08:54):

Nat.leb_gt should help. Also: https://coq.inria.fr/refman/addendum/micromega.html (lia tactic)

view this post on Zulip zohaze (Sep 12 2021 at 14:02):

Very good reference.

Last updated: Sep 26 2023 at 13:01 UTC