proposition: Lemma pNonSingular: 4 * pA * pA * pA + 27 * pB * pB <> 0.
proof: Proof. assert (F1 := p_pos). intros H; generalize (znz_inj _ _ _ H). unfold pkO,pkI,pA, pB, to_p, zero, one, pkplus, GZnZ.add, pkmul, mul, val. repeat match goal with |- ?t = 0 mod p -> _ => rmod t; auto end. rewrite (Zmod_small 0); auto with zarith. intros H1. apply (fun H HH => rel_prime_mod H HH H1). generalize (prime_ge_2 _ p_prime); auto with zarith. apply rel_prime_sym; auto. apply rel_prime_div with N; try apply p_div_N. generalize NonSingular. repeat rewrite Zmult_assoc; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod