Std.TreeMap.getEntryLT?_is_lt

Stream: Is there code for X?

[Dillon Shaffer]

Is there a lemma for

theorem Std.TreeMap.getEntryLT?_is_lt
    [...]
    {tree : STd.TreeMap K V}
    (v : tree.getEntryLT? key = some (key_lt, _))
: key_lt < key
:= sorry

[Markus Himmel]

We don't have lemmas for getEntryLT? yet. It's on our TODO list, but if you or anyone else would like to contribute it, you're very welcome to. Just send me a message, I'll be happy to guide you through the details.

[Dillon Shaffer]

I can't make any promises but I could give it a go, it would certainly be useful for my research so I may be able to allocate time to it