Theorem NNReal.rpow_lt_one_of_one_lt_of_neg

Modification history