feat(Order/Interval/Set/Monotone): strictMono_of_lt_succ (#16732)

Prove `strictMono_of_lt_succ` and `strictAnti_of_pred_lt` for archimedean orders.

Mathlib/Order/Interval/Set/Monotone.lean

@@ -188,10 +188,18 @@ theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : 
   refine hψ _ (lt_of_lt_of_le ?_ hy)
   rwa [Function.iterate_succ', Function.comp_apply, lt_succ_iff_not_isMax]
 
+theorem strictMono_of_lt_succ [SuccOrder α] [IsSuccArchimedean α]
+    (hψ : ∀ m, ψ m < ψ (succ m)) : StrictMono ψ := fun _ _ h ↦
+  (strictMonoOn_Iic_of_lt_succ fun m _ ↦ hψ m) h.le le_rfl h
+
 theorem strictAntiOn_Iic_of_succ_lt [SuccOrder α] [IsSuccArchimedean α] {n : α}
     (hψ : ∀ m, m < n → ψ (succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n) := fun i hi j hj hij =>
   @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij
 
+theorem strictAnti_of_pred_lt [SuccOrder α] [IsSuccArchimedean α]
+    (hψ : ∀ m, ψ (succ m) < ψ m) : StrictAnti ψ := fun _ _ h ↦
+  (strictAntiOn_Iic_of_succ_lt fun m _ ↦ hψ m) h.le le_rfl h
+
 theorem strictMonoOn_Ici_of_pred_lt [PredOrder α] [IsPredArchimedean α] {n : α}
     (hψ : ∀ m, n < m → ψ (pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n) := fun i hi j hj hij =>
   @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij