Theorem Real.logb_ne_zero_of_pos_of_ne_one

Modification history