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