proposition: Lemma strong_spec_irred : forall n d, (NN.to_Z d <> 0%Z) -> let (n',d') := irred n d in Z.gcd (ZZ.to_Z n') (NN.to_Z d') = 1%Z.
proof: Proof. unfold irred; intros. nzsimpl. destr_zcompare; simpl; auto. elim H. apply (Z.gcd_eq_0_r (ZZ.to_Z n)). generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. nzsimpl. rewrite Zgcd_1_rel_prime. apply Zis_gcd_rel_prime. generalize (NN.spec_pos d); lia. generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. apply Zgcd_is_gcd; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig