proposition: Lemma pis_zero_correct: forall k: pK, pis_zero k = true <-> k = 0.
proof: Proof. assert (F0 := p_pos). intros (k, Hk); generalize Hk; case k; simpl. intros Hk1; split; auto; intros H; unfold pkO, zero. apply (zirr p); rewrite Zmod_small; auto with zarith. intros Hk1; split; auto; intros H; try discriminate. intros Hk1; split; auto; intros H; try discriminate. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod