proposition: Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).
proof: Proof. apply Bool.eq_iff_eq_true. rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare. split; [now destruct Z.compare | now intros ->]. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig