Commit 2023-07-24 07:51 16563e08
View on Github →feat: lemmas about List.maximum (#6062)
No particular objection if we only want one out of the _ne_nil and _length_pos pairs, but I like wall-to-wall coverage so exact? always works. :-)
(For context, the place I needed these more naturally wanted the _length_pos lemmas.)