proposition: Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
proof: Proof. intros. replace (Qred [Qq p q]) with (Qred [norm p q]) by (apply Qred_complete; apply spec_norm). symmetry; apply Qred_identity. unfold norm. assert (Hp := NN.spec_pos (Zabs_N p)). assert (Hq := NN.spec_pos q). nzsimpl. destr_zcompare; rewrite ?strong_spec_check_int. qsimpl. qsimpl. rewrite Zgcd_1_rel_prime. destruct (Z_lt_le_dec 0 (NN.to_Z q)). apply Zis_gcd_rel_prime; auto with zarith. apply Zgcd_is_gcd. replace (NN.to_Z q) with 0%Z in * by lia. rewrite Zdiv_0_l in *; lia. simpl; auto with zarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig