proposition: Lemma scalL_prime: let a := ntriple (Z2z (exx.(vx))) (Z2z (exx.(vy))) c1 in let isc := (Z2z 4) ** A ** A ** A ++ (Z2z 27) ** B ** B in let (a1, sc1) := scal isc a exx.(vS) in let (S1,R1) := psplit exx.(vR) in let (a2, sc2) := scal sc1 a1 S1 in let (a3, sc3) := scalL sc2 a2 R1 in match a3 with nzero => if (Zeq_bool (Z.gcd (z2Z sc3) exx.(vN)) 1) then prime exx.(vN) else True | _ => True end.
proof: Proof. intros a isc. case_eq (scal isc a (vS exx)); intros a1 sc1 Ha1. case_eq (psplit (vR exx)); intros S1 R1 HS1. case_eq (scal sc1 a1 S1); intros a2 sc2 Ha2. case_eq (scalL sc2 a2 R1); intros a3 sc3; case a3; auto. intros Ha3; case_eq (Zeq_bool (Z.gcd (z2Z sc3) (vN exx)) 1); auto. intros H1. assert (F0: (vy exx mod vN exx) ^ 2 mod vN exx = ((vx exx mod vN exx) ^ 3 + vA exx * (vx exx mod vN exx) + vB exx) mod vN exx). generalize exxs.(inC). simpl; unfold Zpower_pos; simpl. repeat rewrite Zmult_1_r. intros HH. match goal with |- ?t1 = ?t2 => rmod t1; auto end. rewrite HH. rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. apply f_equal2 with (f := Z.modulo); auto. apply f_equal2 with (f := Zplus); auto. rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. apply f_equal2 with (f := Z.modulo); auto. apply f_equal2 with (f := Zplus); auto. rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. apply f_equal2 with (f := Z.modulo); auto. apply f_equal2 with (f := Zmult); auto. rewrite Zmod_mod; auto. match goal with |- ?t1 = ?t2 => rmod t2; auto end. rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. apply f_equal2 with (f := Z.modulo); auto. rewrite Zmod_mod; auto. generalize (@ZEll.scalL_prime exx.(vN) (exx.(vx) mod exx.(vN)) (exx.(vy) mod exx.(vN)) exx.(vA) exx.(vB) exxs.(n_pos) exxs.(n2_div) exx.(vR) exxs.(lprime) exx.(vS) exxs.(lbig) F0); simpl. generalize (@scal_wf (vS exx) a isc) (@scal_correct (vS exx) a isc). unfold isc. rewrite nplusz; auto; try nw; auto. repeat rewrite nmulz; auto; try nw; auto. repeat rewrite z2Zx. repeat rewrite wwA || rewrite wwB|| rewrite mww. replace (e2E a) with (ZEll.ntriple (vx exx mod vN exx) (vy exx mod vN exx) 1). case ZEll.scal. fold isc; rewrite HS1; rewrite Ha1; simpl; auto. intros r1 rsc1 HH1 HH2. case HH1; clear HH1. unfold c1; repeat split; red; try apply z2Zx1. unfold isc; nw. case HH2; clear HH2. unfold c1; repeat split; red; try apply z2Zx1. unfold isc; nw. intros U1 U2 W1 W2; subst r1 rsc1. generalize (@scal_wf S1 a1 sc1) (@scal_correct S1 a1 sc1). case ZEll.scal. intros r1 rsc1 HH1 HH2. case HH1; clear HH1; auto. case HH2; clear HH2; auto. rewrite Ha2; simpl. intros U1 U2 W3 W4; subst r1 rsc1. generalize (@scalL_wf R1 a2 sc2) (@scalL_correct R1 a2 sc2). case ZEll.scalL. intros n; case n; auto. rewrite Ha3; simpl. intros rsc1 HH1 HH2. case HH1; clear HH1; auto. case HH2; clear HH2; auto. intros _ U2 _ W5; subst rsc1. rewrite H1; auto. intros x1 y1 z1 sc4; rewrite Ha3; simpl; auto. intros _ HH; case HH; auto. intros; discriminate. unfold a; simpl. unfold c1; repeat rewrite z2Zx. rewrite (Zmod_small 1); auto. generalize exxs.(n_pos). auto with zarith. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod