Commit 2021-06-20 21:36 767901ab
View on Github →feat(algebra/ordered_ring): a + 1 ≤ 2 * a (#7995)
Prove one lemma, useful for the Liouville PR #4301. The placement of the lemma will change, once the ordered refactor will get to ordered_ring.