fix(proofs): comprehensively nat-annotate EchidnaNat to green the Isabelle base (#282)

## What

Final pass to make the cron's **Isabelle base** job green (the prior PRs
fixed errors
incrementally, but Isabelle reports polymorphic-lemma failures in
*batches*, so each round
surfaced a new layer). This annotates **every** remaining polymorphic
lemma in `EchidnaNat`
`:: nat` in one go — `power_*`, `le_*`/`less_*`,
`add_le_mono`/`add_less_mono`, the addition
cancellation laws, `div_*`/`mod_*`, `even_*`, and
`strong_induction_example`. `suc_*` stay
as-is (`Suc` already forces nat). All proof bodies are unchanged.

After this, all four base theories (Basic, EchidnaList, EchidnaNat,
Propositional) should
verify on Isabelle2025-2: every statement is now nat-typed, so the
standard `by simp`/`by auto`
proofs discharge, and the earlier genuine gaps (`factorial_monotone`,
`list_all_filter`,
`map_rev`) were already repaired in #281.

## Scope

Per the agreed plan ("finish Isabelle base only"): GroupTheory + Mizar
remain excluded/descoped
and are tracked in **#280** for dedicated, locally-tested repair. This
PR is EchidnaNat-only.

## Verification

Isabelle is `403`-blocked in the dev sandbox, so this is verified by the
cron's Isabelle job on
GitHub runners (Isabelle2025-2). The comprehensive annotation preempts
the batch-reveal cycle,
so it should go green rather than surfacing another layer.

🤖 Generated with [Claude Code](https://claude.com/claude-code)


---
_Generated by [Claude
Code](https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/isabelle/EchidnaNat.thy

@@ -194,27 +194,27 @@ text \<open>
 \<close>
 
 lemma power_zero:
-  "n ^ 0 = 1"
+  "(n::nat) ^ 0 = 1"
   by simp
 
 lemma power_one:
-  "n ^ 1 = n"
+  "(n::nat) ^ 1 = n"
   by simp
 
 lemma power_add:
-  "n ^ (m + p) = n ^ m * n ^ p"
+  "(n::nat) ^ (m + p) = n ^ m * n ^ p"
   by (simp add: power_add)
 
 lemma power_mult:
-  "n ^ (m * p) = (n ^ m) ^ p"
+  "(n::nat) ^ (m * p) = (n ^ m) ^ p"
   by (simp add: power_mult)
 
 text \<open>
   Explicit inductive proof for power addition law.
 \<close>
 
 lemma power_add_inductive:
-  shows "n ^ (m + p) = n ^ m * n ^ p"
+  shows "(n::nat) ^ (m + p) = n ^ m * n ^ p"
 proof (induction m)
   case 0
   show ?case by simp
@@ -240,31 +240,31 @@ text \<open>
 \<close>
 
 lemma le_refl:
-  "n \<le> n"
+  "(n::nat) \<le> n"
   by simp
 
 lemma le_trans:
-  "m \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> m \<le> p"
+  "(m::nat) \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> m \<le> p"
   by simp
 
 lemma le_antisym:
-  "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
+  "(m::nat) \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
   by simp
 
 text \<open>
   Strict ordering properties.
 \<close>
 
 lemma less_irrefl:
-  "\<not>(n < n)"
+  "\<not>((n::nat) < n)"
   by simp
 
 lemma less_trans:
-  "m < n \<Longrightarrow> n < p \<Longrightarrow> m < p"
+  "(m::nat) < n \<Longrightarrow> n < p \<Longrightarrow> m < p"
   by simp
 
 lemma less_imp_le:
-  "m < n \<Longrightarrow> m \<le> n"
+  "(m::nat) < n \<Longrightarrow> m \<le> n"
   by simp
 
 text \<open>
@@ -290,23 +290,23 @@ text \<open>
 \<close>
 
 lemma add_le_mono:
-  "m \<le> n \<Longrightarrow> m + p \<le> n + p"
+  "(m::nat) \<le> n \<Longrightarrow> m + p \<le> n + p"
   by simp
 
 lemma add_less_mono:
-  "m < n \<Longrightarrow> m + p < n + p"
+  "(m::nat) < n \<Longrightarrow> m + p < n + p"
   by simp
 
 text \<open>
   Cancellation laws for addition.
 \<close>
 
 lemma add_left_cancel:
-  "p + m = p + n \<longleftrightarrow> m = n"
+  "(p::nat) + m = p + n \<longleftrightarrow> m = n"
   by simp
 
 lemma add_right_cancel:
-  "m + p = n + p \<longleftrightarrow> m = n"
+  "(m::nat) + p = n + p \<longleftrightarrow> m = n"
   by simp
 
 section \<open>Division and Modulo\<close>
@@ -316,27 +316,27 @@ text \<open>
 \<close>
 
 lemma div_mult_self:
-  "n > 0 \<Longrightarrow> (m * n) div n = m"
+  "(n::nat) > 0 \<Longrightarrow> (m * n) div n = m"
   by simp
 
 lemma mod_mult_self:
-  "n > 0 \<Longrightarrow> (m * n) mod n = 0"
+  "(n::nat) > 0 \<Longrightarrow> (m * n) mod n = 0"
   by simp
 
 lemma div_less:
-  "m < n \<Longrightarrow> n > 0 \<Longrightarrow> m div n = 0"
+  "(m::nat) < n \<Longrightarrow> n > 0 \<Longrightarrow> m div n = 0"
   by simp
 
 lemma mod_less:
-  "m < n \<Longrightarrow> n > 0 \<Longrightarrow> m mod n = m"
+  "(m::nat) < n \<Longrightarrow> n > 0 \<Longrightarrow> m mod n = m"
   by simp
 
 text \<open>
   Division-modulo identity.
 \<close>
 
 lemma div_mod_equality:
-  "n > 0 \<Longrightarrow> (m div n) * n + m mod n = m"
+  "(n::nat) > 0 \<Longrightarrow> (m div n) * n + m mod n = m"
   by simp
 
 section \<open>Even and Odd\<close>
@@ -346,31 +346,31 @@ text \<open>
 \<close>
 
 lemma even_zero:
-  "even 0"
+  "even (0::nat)"
   by simp
 
 lemma even_double:
-  "even (2 * n)"
+  "even (2 * (n::nat))"
   by simp
 
 lemma even_succ_succ:
-  "even n \<longleftrightarrow> even (Suc (Suc n))"
+  "even (n::nat) \<longleftrightarrow> even (Suc (Suc n))"
   by simp
 
 text \<open>
   Sum of two even numbers is even.
 \<close>
 
 lemma even_add:
-  "even m \<Longrightarrow> even n \<Longrightarrow> even (m + n)"
+  "even (m::nat) \<Longrightarrow> even n \<Longrightarrow> even (m + n)"
   by simp
 
 text \<open>
   Product involving an even number is even.
 \<close>
 
 lemma even_mult:
-  "even m \<or> even n \<Longrightarrow> even (m * n)"
+  "even (m::nat) \<or> even n \<Longrightarrow> even (m * n)"
   by auto
 
 section \<open>Strong Induction\<close>
@@ -382,8 +382,8 @@ text \<open>
 \<close>
 
 lemma strong_induction_example:
-  assumes "\<And>n. (\<forall>m. m < n \<longrightarrow> P m) \<Longrightarrow> P n"
-  shows "P n"
+  assumes "\<And>k::nat. (\<forall>m. m < k \<longrightarrow> P m) \<Longrightarrow> P k"
+  shows "P (n::nat)"
 proof -
   have "\<forall>m. m \<le> n \<longrightarrow> P m"
   proof (induction n)