proposition: Lemma gt_Z_B2P': forall x y, gtP_Z x y <-> Z.gt x y.
proof: Proof. intros x y; split; intro H. unfold gtP_Z in H. case_eq ((x >? y)%Z ); intros; rewrite H0 in H; try easy. now apply Zgt_is_gt_bool in H0. apply gt_Z_B2P. now apply Zgt_is_gt_bool. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes