feat(algebra/order/monoid) Add zero_le_three and zero_le_four (#15219)

leanprover-community · Jul 10, 2022 · f51aaab · f51aaab
1 parent e5b8d09
commit f51aaab
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/algebra/order/monoid.lean b/src/algebra/order/monoid.lean
@@ -120,6 +120,14 @@ lemma zero_le_two [preorder α] [has_one α] [add_zero_class α] [zero_le_one_cl
   [covariant_class α α (+) (≤)] : (0 : α) ≤ 2 :=
 add_nonneg zero_le_one zero_le_one
 
+lemma zero_le_three [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
+  [covariant_class α α (+) (≤)] : (0 : α) ≤ 3 :=
+add_nonneg zero_le_two zero_le_one
+
+lemma zero_le_four [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α]
+  [covariant_class α α (+) (≤)] : (0 : α) ≤ 4 :=
+add_nonneg zero_le_two zero_le_two
+
 lemma one_le_two [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α]
   [covariant_class α α (+) (≤)] : (1 : α) ≤ 2 :=
 calc 1 = 1 + 0 : (add_zero 1).symm