Mathlib v4.30 source proposition Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

The p-adic valuation step, bridged to a Nat-level core via X := natAbs m, Y := natAbs n (nat_abs_dvd_nat_abs_of_dvd/dvd_of_nat_abs_dvd/nat_abs_mul, the same bridging style gcd.rs's own Int.euclid_lemma uses). The Nat-level core: eliminate X = p^k*x', Y = p^l*y' (Nat.dvd elimination, a local dvd_elim/dvd_intro copy of the pattern nat_prelude keeps per-file), regroup X*Y = p^(k+l)*(x'*y') via a four-factor regroup ((a*b)*(c*d) = (a*c)*(b*d), a local copy of nat_prelude/dvd_mul_split.rs's private mul_mul_mul_comm) and the already-proved Nat.pow_add, cancel the positive factor p^(k+l) from p^(k+l+1) ∣ X*Y (Nat.pow_pos for positivity, Nat.mul_left_cancel_of_pos for the cancellation itself, wrapped in a local dvd_cancel_left_of_pos copy of the pattern nat_prelude/dvd_mul_split.rs and lcm_gcd_lemmas.rs keep per-file) to get p ∣ x'*y', then the already-proved Nat.euclid_lemma gives p ∣ x' or p ∣ y', each of which regroups back (via Nat.mul_assoc) to p^(k+1) ∣ X or p^(l+1) ∣ Y. Every exponent-arithmetic step (k+l+1 = succ(k+l), p^(succ n) = p^n*p) is a defeq bridge resolved by the kernel's own reduction, not an explicit rewrite -- Nat.add and Nat.pow are BOTH defined by right-recursion in this kernel, so their successor cases are refl-provable defining equations (the same fact that makes Nat.mul_succ refl-provable; verified by isolating a first attempt's TypeMismatch with a throwaway Kernel::render_lean-based debug probe, which found an unrelated missing Or-wrap rather than any exponent-arithmetic gap). int_theorem_inventory's rendered type for Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul matches this fact's formal.statement exactly. New proof, lane int-prime-dvd (2026-09-01): crates/axeyum-lean-kernel/src/int_prelude/prime_dvd_mul_mirrors.rs. No Nat declaration was added -- pow_add, pow_pos, mul_left_cancel_of_pos, mul_assoc, mul_comm, euclid_lemma, le_add_right, le_trans, dvd (the Exists-based predicate), and the Exists/Or/And recursors are all pre-existing.

prelude_axiom_inventory --require-axiom-free integer enumerates the built Int environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration (measured: integer: axiom=0, exit 0; the axreal: axiom=30 row is the separate legacy axiomatized-reals package, unrelated to this declaration -- see CLAUDE.md's AxReal/CReal gotcha). A theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds this declaration's own footprint by []. int_prelude_tests::every_int_declaration_is_checked_and_axiom_free additionally checks this theorem's own Kernel::axiom_footprint directly via derived_lemmas (it is listed there).