fact: Fixpoint ult_big_endian_lit_list (bs1 bs2: list _lit) := match bs1, bs2 with | nil, _ => Clit (Lit._false) | _, nil => Clit (Lit._false) | xi :: nil, yi :: nil => (Cand (Clit (Lit.neg xi)) (Clit yi)) | xi :: x', yi :: y' => (Cor (Cand (Ciff (Clit xi) (Clit yi)) (ult_big_endian_lit_list x' y')) (Cand (Clit (Lit.neg xi)) (Clit yi))) end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance