proposition: Theorem spec_leb x y : leb x y = Z.leb [x] [y].
proof: Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. now destruct Z.compare; split. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen