strict_mono on int

Stream: Is there code for X?

[Yury G. Kudryashov]

I can find neither of these for int:

• docs#nat.le_rec_on / docs#nat.le_induction;
• docs#monotone_nat_of_le_succ / docs#strict_mono_nat_of_lt_succ
  Do we have either of these?

[Yury G. Kudryashov]

(I'm going to add *mono*_of_* lemmas)

[Yaël Dillies]

Nope, I meant to add the more general versions using docs#succ_order but never did. Feel free to add int versions.

[Yury G. Kudryashov]

#10895