pub fn prove_nonzero(ctx: &Context, r: &Rational) -> Option<Term>Expand description
Prove r ≠ 0 in the kernel by EXHIBITING its inverse: a kernel-checked proof of r·(1/r) = 1.
A value with a multiplicative inverse is nonzero, so this certifies nonsingularity when applied to
a determinant. None iff r == 0 — correctly unprovable, since 0 has no inverse.