proposition: Lemma pone_not_zero: 1 <> 0.
proof: Proof. intros H; generalize (znz_inj _ _ _ H); simpl val. repeat (rewrite Zmod_small); generalize (prime_ge_2 _ p_prime); auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod