inequality following from an equality

Stream: new members

[Andre Popovitch]

If in my goal view I have

eq : succ h + 0 = a

is there a way to create

eq : succ h >= a

?

[Johan Commelin]

Does have foo : succ h ≥ a, by library_search help?

[Andre Popovitch]

I'm playing the game haha. I get unknown identifier 'library_search'

[Andre Popovitch]

But if I can create ∃ (c, succ h + c = a), which I think I ought to be able to with c = 0, I think that would be sufficient

[Patrick Johnson]

replace eq : succ h ≥ a := ge_of_eq eq

[Andre Popovitch]

That works, thanks! Is there a way to create the existential directly?

[Patrick Johnson]

have h : ∃ c, succ h + c = a := ⟨0, eq⟩

or

have h : succ h ≥ a := ⟨0, eq⟩

[Andre Popovitch]

woah, thank you

[Andre Popovitch]

oh, so an ∃ is just a tuple where the type of the second element can depend on the value of the first element?