proposition: Theorem spec_norm: forall n q, [norm n q] == [Qq n q].
proof: Proof. intros p q; unfold norm. assert (Hp := NN.spec_pos (Zabs_N p)). assert (Hq := NN.spec_pos q). nzsimpl. destr_zcompare. rewrite strong_spec_check_int; reflexivity. rewrite strong_spec_check_int. qsimpl. generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). lia. replace (NN.to_Z q) with 0%Z in * by (symmetry; assumption). rewrite Zdiv_0_l in *; auto with zarith. apply Zgcd_div_swap0; lia. qsimpl. assert (H' : Z.gcd (ZZ.to_Z p) (NN.to_Z q) = 0%Z). generalize (Z.gcd_nonneg (ZZ.to_Z p) (NN.to_Z q)); lia. symmetry; apply (Z.gcd_eq_0_l _ _ H'); auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig