proposition: Theorem spec_compare : forall x y, compare x y = Z.compare [x] [y].
proof: Proof. intros x y. rewrite compare_fold. apply spec_iter_sym; clear x y. intros. apply ZnZ.spec_compare. intros. cbv beta zeta. apply spec_comparen_m. intros n m x y; unfold comparenm. rewrite (spec_cast_l n m x), (spec_cast_r n m y). unfold to_Z; apply ZnZ.spec_compare. intros. subst. now rewrite <- Z.compare_antisym. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen