proposition: Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d].
proof: Proof. intros; unfold check_int. nzsimpl. destr_zcompare. simpl. rewrite <- H; qsimpl. congruence. reflexivity. qsimpl. lia. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig