system of inequalities

Stream: new members

[Valéry Croizier]

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]

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

[Valéry Croizier]

thanks

[Jalex Stark]

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}