proposition: Lemma ztest: forall x y, x ?= y =Zeq_bool (z2Z x) (z2Z y).
proof: Proof. intros x y. unfold neq. rewrite (ZnZ.spec_compare x y); case Z.compare_spec; intros HH; match goal with H: context[x] |- _ => generalize H; clear H; intros HH1 end. symmetry; apply GZnZ.Zeq_iok; auto. case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; intros HH; rewrite HH; auto with zarith. case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; intros HH; rewrite HH; auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod