Theorem Real.log_ne_zero_of_pos_of_ne_one

Modification history