proposition: Lemma spec_irred_zero : forall n d, (NN.to_Z d = 0)%Z <-> (NN.to_Z (snd (irred n d)) = 0)%Z.
proof: Proof. intros. unfold irred. split. nzsimpl; intros. destr_zcompare; auto. simpl. nzsimpl. rewrite H, Zdiv_0_l; auto. nzsimpl; destr_zcompare; simpl; auto. nzsimpl. intros. generalize (NN.spec_pos d); intros. destruct (NN.to_Z d); auto. assert (0 < 0)%Z. rewrite <- H0 at 2. apply Zgcd_div_pos; auto with zarith. compute; auto. discriminate. compute in H1; elim H1; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig