mathlib3

feat(data/fin*): uniqueness of increasing bijection

#2258

Merged