basic): merge `fin.rev` and `order_iso.fin_equiv` (#16745)

Commit

3 years ago

refactor(data/fin/basic): merge `fin.rev` and `order_iso.fin_equiv` (#16745) Also add some missing lemmas.

Author

urkud

Parents