nnreal): shorter proof of `div_lt_iff` (#5945)

Commit

5 years ago

refactor(data/real/nnreal): shorter proof of `div_lt_iff` (#5945) Co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents