Really simple question about decide

Stream: lean4

[Casavaca]

Could anyone tell me how to prove this?

example (m n : Nat) (h : decide (m < n) = true) : m < n := sorry

[Mario Carneiro]

I think it's called docs4#of_decide_eq_true

[Mario Carneiro]

or by library_search if you're into that kind of thing

[Casavaca]

Thanks.
Do you know how to tell library_search to print hints?