Theorem Rat.AbsoluteValue.one_lt_of_not_bounded

Modification history