From 767901ab594375a1335bb324f88d5be01af1367b Mon Sep 17 00:00:00 2001 From: damiano Date: Sun, 20 Jun 2021 21:36:12 +0000 Subject: [PATCH] =?UTF-8?q?feat(algebra/ordered=5Fring):=20`a=20+=201=20?= =?UTF-8?q?=E2=89=A4=202=20*=20a`=20(#7995)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. --- src/algebra/ordered_ring.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean index 427851dd9e104..2f30765e068c2 100644 --- a/src/algebra/ordered_ring.lean +++ b/src/algebra/ordered_ring.lean @@ -16,6 +16,12 @@ set_option old_structure_cmd true universe u variable {α : Type u} +lemma add_one_le_two_mul [preorder α] [semiring α] [covariant_class α α (+) (≤)] + {a : α} (a1 : 1 ≤ a) : + a + 1 ≤ 2 * a := +calc a + 1 ≤ a + a : add_le_add_left a1 a + ... = 2 * a : (two_mul _).symm + /-- An `ordered_semiring α` is a semiring `α` with a partial order such that multiplication with a positive number and addition are monotone. -/ @[protect_proj]