proposition: Lemma index_seq_strictly_incr : ∀ n : ℕ → ℕ, is_index_seq n ⇒ (is_increasing (fun (k : ℕ) ↦ (n k - k)%nat)).
proof: Proof. Take n : (ℕ → ℕ); such that (is_index_seq n). We need to show that (for all k : ℕ, (n(k) - k ≤ n(S(k)) - S(k))%nat). Take k : ℕ. It holds that (for all k0 : ℕ, (n k0 < n (S k0))%nat). It holds that (n k < n (S k))%nat. We conclude that (n k - k ≤ n (S k) - S k)%nat. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove