Lemmas about inequalities with 1.

theorem one_le_dite {α : Type u_1} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), 1 ≤ a h) (hb : ∀ (h : ¬p), 1 ≤ b h) : 1 ≤ dite p a b

theorem dite_nonneg {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), 0 ≤ a h) (hb : ∀ (h : ¬p), 0 ≤ b h) : 0 ≤ dite p a b

theorem dite_le_one {α : Type u_1} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), a h ≤ 1) (hb : ∀ (h : ¬p), b h ≤ 1) : dite p a b ≤ 1

theorem dite_nonpos {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), a h ≤ 0) (hb : ∀ (h : ¬p), b h ≤ 0) : dite p a b ≤ 0

theorem one_lt_dite {α : Type u_1} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), 1 < a h) (hb : ∀ (h : ¬p), 1 < b h) : 1 < dite p a b

theorem dite_pos {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), 0 < a h) (hb : ∀ (h : ¬p), 0 < b h) : 0 < dite p a b

theorem dite_lt_one {α : Type u_1} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), a h < 1) (hb : ∀ (h : ¬p), b h < 1) : dite p a b < 1

theorem dite_neg {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), a h < 0) (hb : ∀ (h : ¬p), b h < 0) : dite p a b < 0

theorem one_le_ite {α : Type u_1} [One α] {p : Prop} [Decidable p] {a b : α} [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ if p then a else b

theorem ite_nonneg {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a b : α} [LE α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ if p then a else b

theorem ite_le_one {α : Type u_1} [One α] {p : Prop} [Decidable p] {a b : α} [LE α] (ha : a ≤ 1) (hb : b ≤ 1) : (if p then a else b) ≤ 1

theorem ite_nonpos {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a b : α} [LE α] (ha : a ≤ 0) (hb : b ≤ 0) : (if p then a else b) ≤ 0

theorem one_lt_ite {α : Type u_1} [One α] {p : Prop} [Decidable p] {a b : α} [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < if p then a else b

theorem ite_pos {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a b : α} [LT α] (ha : 0 < a) (hb : 0 < b) : 0 < if p then a else b

theorem ite_lt_one {α : Type u_1} [One α] {p : Prop} [Decidable p] {a b : α} [LT α] (ha : a < 1) (hb : b < 1) : (if p then a else b) < 1

theorem ite_neg {α : Type u_1} [Zero α] {p : Prop} [Decidable p] {a b : α} [LT α] (ha : a < 0) (hb : b < 0) : (if p then a else b) < 0