Theorem Real.neg_one_lt_goldenConj

Modification history