proposition: Lemma inversible_is_not_k0: forall x, [x] -> x :%p <> 0.
proof: Proof. intros x1 (k, Hk) H1. assert (F2: 2 < p). case (Zle_lt_or_eq _ _ (prime_ge_2 p p_prime)); auto. intros HH1; case N_not_div_2; rewrite HH1. apply p_div_N. assert (F3:= N_lt_2). injection H1; clear H1; rewrite (Zmod_small 0); auto with zarith; intros HH. absurd ((x1 * k) mod p = ((x1 * k) mod N) mod p). rewrite Hk. rewrite Zmult_mod; auto with zarith. rewrite HH; rewrite Zmult_0_l. repeat rewrite Zmod_small; auto with zarith. apply Zmod_div_mod; auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod