golden_ratio): simpler proof of `gold_pos` (#5910)

Commit

4 years ago

refactor(data/real/golden_ratio): simpler proof of `gold_pos` (#5910) 13X smaller (pretty-printed) proof term Co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents