proposition: Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].
proof: Proof. apply eq_iff_eq_true. unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare. split; [now destruct Z.compare | now intros ->]. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen