pub fn at_least(vars: &[ProofExpr], k: usize, aux: &str) -> ProofExpr
“At least k of vars are true” — i.e. at most n−k are false.
k
vars
n−k