fact: Definition check_slt (bs1 bs2: list _lit) (bsres: _lit) : bool := if Lit.is_pos bsres then eq_carry_lit (slt_lit_list bs1 bs2) bsres else false.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance