Function verify_ring 

pub fn verify_ring(goal: &Syn) -> bool

try_ring goal reduces to DRingSolve goal, verified here.

The gate is the first kernel’s: a three-argument Eq ty lhs rhs whose ty is Int or Nat, both sides inside the add/sub/mul fragment. div and mod fall out of poly_bounds exactly as ring::reify refuses them.