fact: Definition check_concat (bs1 bs2 bsres: list _lit) : bool := if (forallb2 eq_carry_lit (lit_to_carry (bs2 ++ bs1)) bsres) then true 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