[Merged by Bors] - refactor: New Colex API

Mathlib/Algebra/BigOperators/Order.lean

@@ -548,6 +548,18 @@ theorem prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
 #align finset.prod_eq_prod_iff_of_le Finset.prod_eq_prod_iff_of_le
 #align finset.sum_eq_sum_iff_of_le Finset.sum_eq_sum_iff_of_le
 
+variable [DecidableEq ι]
+
+@[to_additive] lemma prod_sdiff_le_prod_sdiff :
+    ∏ i in s \ t, f i ≤ ∏ i in t \ s, f i ↔ ∏ i in s, f i ≤ ∏ i in t, f i := by
+  rw [←mul_le_mul_iff_right, ←prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter, ←prod_union,
+    inter_comm, sdiff_union_inter]; simpa only [inter_comm] using disjoint_sdiff_inter t s
+
+@[to_additive] lemma prod_sdiff_lt_prod_sdiff :
+    ∏ i in s \ t, f i < ∏ i in t \ s, f i ↔ ∏ i in s, f i < ∏ i in t, f i := by
+  rw [←mul_lt_mul_iff_right, ←prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter, ←prod_union,
+    inter_comm, sdiff_union_inter]; simpa only [inter_comm] using disjoint_sdiff_inter t s
+
 end OrderedCancelCommMonoid
 
 section LinearOrderedCancelCommMonoid

Mathlib/Algebra/GeomSum.lean

@@ -584,3 +584,21 @@ theorem geom_sum_neg_iff [LinearOrderedRing α] (hn : n ≠ 0) :
 #align geom_sum_neg_iff geom_sum_neg_iff
 
 end Order
+
+variable {m n : ℕ} {s : Finset ℕ}
+
+/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
+`m ≥ 2` is less than `m ^ n`. -/
+lemma Nat.geomSum_eq (hm : 2 ≤ m) (n : ℕ) :
+    ∑ k in range n, m ^ k = (m ^ n - 1) / (m - 1) := by
+  refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) $ tsub_eq_of_eq_add ?_).symm
+  simpa only [tsub_add_cancel_of_le $ one_le_two.trans hm, eq_comm] using geom_sum_mul_add (m - 1) n
+
+/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
+`m ≥ 2` is less than `m ^ n`. -/
+lemma Nat.geomSum_lt (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k in s, m ^ k < m ^ n :=
+  calc
+    ∑ k in s, m ^ k ≤ ∑ k in range n, m ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk
+    _ = (m ^ n - 1) / (m - 1) := Nat.geomSum_eq hm _
+    _ ≤ m ^ n - 1 := Nat.div_le_self _ _
+    _ < m ^ n := tsub_lt_self (by positivity) zero_lt_one