lemma proved term proof

`phi_rpow_neg_lt_of_lt`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 260lemma phi_rpow_neg_lt_of_lt {y z : ℝ} (hyz : y < z) :
 261    goldenRatio ^ (-z) < goldenRatio ^ (-y) :=

Term-mode proof.

 262  phi_rpow_strictMono (neg_lt_neg hyz)
 263
 264end IndisputableMonolith.Numerics

Lean names referenced from this declaration's body.