Function conditional_subtract_in_range 

pub fn conditional_subtract_in_range(q: i64) -> bool

Certify that conditional-subtract reduction keeps a modular-ADD result in range. After an addition in 𝔽_q the value a lies in [0, 2q); the reduction is csub(a) = if a ≥ q { a − q } else { a }, and the result must lie in [0, q). The two non-trivial bounds (the a ≥ q branch) are discharged by Fourier-Motzkin: a goal is valid iff its negation’s constraints are UNSAT.