Zulip Chat Archive

Stream: new members

Topic: system of inequalities


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

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

Valéry Croizier (Jul 13 2020 at 20:33):

thanks

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: Dec 20 2023 at 11:08 UTC