proposition: Lemma spec_irred : forall n d, exists g, let (n',d') := irred n d in (ZZ.to_Z n' * g = ZZ.to_Z n)%Z /\ (NN.to_Z d' * g = NN.to_Z d)%Z.
proof: Proof. intros. unfold irred; nzsimpl; simpl. destr_zcompare. exists 1%Z; nzsimpl; auto. exists 0%Z; nzsimpl. assert (Z.gcd (ZZ.to_Z n) (NN.to_Z d) = 0%Z). generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. clear H. split. symmetry; apply (Z.gcd_eq_0_l _ _ H0). symmetry; apply (Z.gcd_eq_0_r _ _ H0). exists (Z.gcd (ZZ.to_Z n) (NN.to_Z d)). simpl. split. nzsimpl. destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)). rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. nzsimpl. destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)). rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig