Zulip Chat Archive

Stream: new members

Topic: system of inequalities


view this post on Zulip Valéry Croizier (Jul 13 2020 at 20:30):

How do you handle this kind of system?
example (a b c d : nat) : a + 1 = b -> c + 1 >= d -> b < d -> a < c

view this post on Zulip Sebastien Gouezel (Jul 13 2020 at 20:31):

example (a b c d : nat) : a + 1 = b -> c + 1 >= d -> b < d -> a < c :=
by omega

view this post on Zulip Valéry Croizier (Jul 13 2020 at 20:33):

thanks

view this post on Zulip Jalex Stark (Jul 13 2020 at 20:36):

omega can prove lots of things about natural numbers. linarith can handle this over other rings

import tactic
example (a b c d : rat) : a + 1 = b -> c + 1 >= d -> b < d -> a < c :=
by {intros, linarith}

Last updated: May 14 2021 at 21:11 UTC