- 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