Theory "arith_utils"

Parents     utils

Theorems

two_children_parent_bound_main_lemma_7
|- ∀x y z a. x ≤ y * a ∧ a ≤ z ⇒ x ≤ y * z
two_children_parent_bound_main_lemma_8
|- ∀a b c d. (a + b) * (c + d) = a * c + a * d + b * c + b * d
two_children_parent_bound_main_lemma_9
|- ∀y z a. a ≤ z ⇒ y * a ≤ y * z
parent_children_main_lemma_1_1_14_2
|- ∀a b c d e. b ≤ d ∧ c ≤ e ⇒ a * b + c ≤ a * d + e
parent_children_main_lemma_1_1_17
|- ∀a b c d. b ≤ c ⇒ a * (b + d) ≤ a * (c + d)
N_gen_valid_thm_1_1_1
|- ∀a b. a * b + b = b * (a + 1)
N_gen_valid_thm_1_1
|- ∀a b x y. a ≤ x ∧ b ≤ y ∧ c ≤ z ⇒ a * b + c ≤ x * y + z
add_less
|- a < x ∧ b ≤ y ⇒ a + b < x + y
add_less_2
|- a < y ∧ b ≤ x ⇒ a + b < x + y
add_less_3
|- a ≤ x ∧ b < y ⇒ a + b < x + y