proposition: Lemma eq_Z_B2P: forall x y, Z.eqb x y = true <-> eqP_Z x y.
proof: Proof. intros x y; split; intro H. unfold eqP_Z; now rewrite H. unfold eqP_Z in H. case_eq ((x =? y)%Z ); intros; try now subst. rewrite H0 in H. now contradict H. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes