Theorem monotone_nat_of_le_succ

Modification history