Theorem Real.abs_mulExpNegMulSq_one_le_one

Modification history