Extra lemmas about canonically ordered monoids

theorem Set.range_add_eq_image_Ici {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {β : Type u_2} {f : α → β} {k : α} : (range fun (x : α) => f (x + k)) = f '' Ici k

theorem lt_add_iff_lt_left_or_exists_lt {α : Type u_1} [LinearOrder α] {a b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : a < b + c ↔ a < b ∨ ∃ (d : α), d < c ∧ a = b + d

theorem forall_lt_add_iff_lt_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∀ (a : α), a < b + c → P a) ↔ (∀ (a : α), a < b → P a) ∧ ∀ (d : α), d < c → P (b + d)

theorem exists_lt_add_iff_lt_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∃ (a : α), a < b + c ∧ P a) ↔ (∃ (a : α), a < b ∧ P a) ∨ ∃ (d : α), d < c ∧ P (b + d)

theorem le_add_iff_lt_left_or_exists_le {α : Type u_1} [LinearOrder α] {a b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : a ≤ b + c ↔ a < b ∨ ∃ (d : α), d ≤ c ∧ a = b + d

theorem forall_le_add_iff_le_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∀ (a : α), a ≤ b + c → P a) ↔ (∀ (a : α), a < b → P a) ∧ ∀ (d : α), d ≤ c → P (b + d)

theorem exists_le_add_iff_le_left {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [Add α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∃ (a : α), a ≤ b + c ∧ P a) ↔ (∃ (a : α), a < b ∧ P a) ∨ ∃ (d : α), d ≤ c ∧ P (b + d)

theorem lt_add_iff_lt_right_or_exists_lt {α : Type u_1} [LinearOrder α] {a b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : a < b + c ↔ a < c ∨ ∃ (d : α), d < b ∧ a = d + c

theorem forall_lt_add_iff_lt_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∀ (a : α), a < b + c → P a) ↔ (∀ (a : α), a < c → P a) ∧ ∀ (d : α), d < b → P (d + c)

theorem exists_lt_add_iff_lt_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α] [IsLeftCancelAdd α] : (∃ (a : α), a < b + c ∧ P a) ↔ (∃ (a : α), a < c ∧ P a) ∨ ∃ (d : α), d < b ∧ P (d + c)

theorem le_add_iff_lt_right_or_exists_le {α : Type u_1} [LinearOrder α] {a b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : a ≤ b + c ↔ a < c ∨ ∃ (d : α), d ≤ b ∧ a = d + c

theorem forall_le_add_iff_le_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∀ (a : α), a ≤ b + c → P a) ↔ (∀ (a : α), a < c → P a) ∧ ∀ (d : α), d ≤ b → P (d + c)

theorem exists_le_add_iff_le_right {α : Type u_1} [LinearOrder α] {P : α → Prop} {b c : α} [AddCommMagma α] [CanonicallyOrderedAdd α] [AddLeftMono α] [IsLeftCancelAdd α] : (∃ (a : α), a ≤ b + c ∧ P a) ↔ (∃ (a : α), a < c ∧ P a) ∨ ∃ (d : α), d ≤ b ∧ P (d + c)