Euclid's lemma: a prime dividing a product divides a factor

`build_nat_prelude` admits this through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so producing the row is a machine-checked proof. Primality is spelled inline as `2 <= p AND forall d, d | p -> d = 1 OR d = p`, matching this fact's `formal.statement` rather than a `Prime` abbreviation -- a fact is only closed by the statement it actually makes. Proof: let g = gcd p a; g | p, so primality splits g = 1 or g = p. If g = p then p = gcd p a | a. If g = 1, Bezout gives naturals with (1 + p*mn) + a*nn = p*mp + a*np; scaling by b puts it in the form b + X = Y with p | X and p | Y (using p | a*b on the a-terms), and `dvd_add_right_cancel_of_pos` yields p | b WITHOUT forming a difference, which is what makes the argument valid over the naturals. The command names its own subject twice over: the example exits non-zero for a name that does not exist, and the grep requires the admitted declaration to be printed. TIGHTENED 2026-08-17: the command matched the NAME only, which a weakened statement survives. Lane `nat-prime-divisor` measured this concretely on its own theorem — spelling a primality bound `1 <= p` instead of `2 <= p` still type-checks, still admits, and passes every name-only checker, while being satisfied by p = 1. The kernel cannot see a weaker statement; only comparing the rendered TYPE can. This now matches the full type exactly (grep -qxF), so any change to the proposition breaks it.

`theorem_axiom_footprint` reports `nat Nat.euclid_lemma 0` and `integer Nat.euclid_lemma 0` directly. `nat_axiom_inventory` bounds it: the enumeration reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, and a theorem cannot depend on a trusted declaration the environment does not contain. Counting `Declaration::Axiom` alone would NOT suffice -- `Opaque` has no proof body and `Quotient` admits `Quot.sound` -- so the enumeration covers all three.