Module arith 

Proof-PRODUCING arithmetic oracle (untrusted search, kernel-checked proof).

Given an Int equality goal Eq Int lhs rhs, prove_int_eq searches for a genuine kernel proof term and returns it — or None. Nothing here is trusted: whatever it returns is re-checked by the kernel’s infer_type, so a wrong proof is rejected, never believed. This is the Coq-lia/nia model — the fast search lives outside the trusted base; a bug here can only cause a failed proof, never a false one.

Trust boundary: closed/literal goals are proven by add/mul computation plus refl (zero axioms). Ring identities are proven from the seven registered commutative-ring axioms (add_comm/add_assoc/add_zero/mul_comm/ mul_assoc/mul_one/mul_distrib_add) — the entire trusted arithmetic base.

Functions

prove_int_eq

Prove an Int equality Eq Int lhs rhs, or return None.