pub fn prove_solve(
ctx: &Context,
a: &[Vec<Rational>],
b: &[Rational],
) -> Option<(Vec<Rational>, Vec<Term>)>Expand description
Solve A·x = b exactly and hand back the exact x together with a kernel-checked proof that it
solves the system (one proof term per row). None iff singular or beyond the i64 oracle width.