proposition: Lemma scalL_prime: let a := ntriple x y 1 in let isc := 4 ** A ** A ** A ++ 27 ** B ** B in let (a1, sc1) := scal N A isc a F in let (S1,R1) := psplit lR in let (a2, sc2) := scal N A sc1 a1 S1 in let (a3, sc3) := scalL N A sc2 a2 R1 in match a3 with nzero => if (Zeq_bool (Z.gcd sc3 N) 1) then prime N else True | _ => True end.
proof: Proof. assert (F0: 0 < N); try auto with zarith. intros a isc. case_eq (scal N A isc a F); intros a1 sc1 Ha1. case_eq (psplit lR); intros S1 R1 HS1. case_eq (scal N A sc1 a1 S1); intros a2 sc2 Ha2. case_eq (scalL N A sc2 a2 R1); intros a3. case a3; auto. intros sc3 Hsc3. generalize (Zeq_bool_eq (Z.gcd sc3 N) 1); case Zeq_bool; intros Hz; auto. case (prime_dec N); auto; intros Hn. case (Zdivide_div_prime_le_square N); auto with zarith. intros p (Hp, (Hp1, Hp2)). pose (p_pos:= GZnZ.p_pos _ Hp). pose (to_p := fun x => mkznz _ _ (modz p x)). assert (Ni1: nInversible N (scalL N A sc2 a2 R1)). rewrite Hsc3; constructor. assert (tmp: Bezout sc3 N 1). apply Zis_gcd_bezout. rewrite <- Hz; auto; apply Zgcd_is_gcd. inversion_clear tmp as [u v Huv]. exists u. rewrite Zmult_comm. rewrite <- Z_mod_plus with (b := v); auto with zarith. rewrite Huv; rewrite Zmod_small; auto with zarith. case nInversible_scalL with (2 := Ni1); auto with zarith. intros Nt1 Nt2. assert (Ni2: nInversible N (scal N A sc1 a1 S1)). rewrite Ha2. inversion_clear Nt1; constructor; auto; repeat itac. case nInversible_scal with (2 := Ni2); auto with zarith. clear Nt1 Nt2; intros Nt1 Nt2. assert (Ni3: nInversible N (scal N A isc a F)). rewrite Ha1. inversion_clear Nt1; constructor; auto; repeat itac. case nInversible_scal with (2 := Ni3); auto with zarith. clear Nt1 Nt2; intros Ni4 Ni5. assert (Rp: rel_prime N (4 * A * A * A + 27 * B * B)). case Ni5; intros z1 Hz1. apply bezout_rel_prime. set (d := 4 * A * A * A + 27 * B * B). apply Bezout_intro with (- ((d * z1)/N)) z1. generalize Hz1; unfold isc. unfold nplus, nmul. rewrite (Zmodml (4 * A)); auto. rewrite (Zmodml (4 * A * A)); auto. rewrite (Zmodml (27 * B)); auto. rewrite <- Zplus_mod; auto. rewrite Zmodml; auto; fold d; clear Hz1; intros Hz1. rewrite (Z_div_mod_eq_full (z1 * d) N). rewrite (Zmult_comm z1). rewrite (Zmult_comm N). rewrite Zplus_assoc. rewrite (fun x y => Zplus_comm (x * y)). rewrite <- Zopp_mult_distr_l. rewrite Zplus_opp_r; auto. pose (pell := pell_theory A B N_not_div_2 Rp Hp Hp1). pose (pequiv := @equiv A B p). assert (Hoc: pow (pkI p) (@pkmul p) (to_p y) 2 = pkplus (pkplus (pow (pkI p) (@pkmul p) (to_p x) 3) (pkmul (pA A p) (to_p x))) (pB B p)). unfold pA, pB, to_p. repeat rewrite <- (to_p_pow N_lt_2 Hp); auto. simpl Z_of_nat. repeat rewrite <- (to_p_nmul N_lt_2 Hp); auto. repeat rewrite <- (to_p_nplus N_lt_2 Hp); auto. apply (zirr p). rewrite (@Zmod_div_mod p N); auto; rewrite on_curve; rewrite <- Zmod_div_mod; auto. unfold nmul, nplus. rewrite (fun xx => @Zmodpr xx (x^3)); auto. rewrite Zmodpl; auto; rewrite <- Zmod_div_mod; auto. pose (pcurve_elt := curve_elt (pkI p) (@pkplus p) (@pkmul p) (pA A p) (pB B p)). assert (E1: pequiv a (pcurve_elt (to_p x) (to_p y) Hoc)). unfold pequiv, a, pcurve_elt. apply n_equiv. unfold pkdiv, div, to_p. fold p_pos; set (pp := mkznz p (x mod p) (modz p x)). fold p_pos; set (p1 := mkznz p (1 mod p) (modz p 1)). pattern pp at 1; rewrite <- ((FZpZ _ Hp).(F_R).(Rmul_1_l) pp). unfold one; fold p_pos; fold p1. rewrite ((FZpZ _ Hp).(F_R).(Rmul_comm) p1). rewrite <- (FZpZ _ Hp).(F_R).(Rmul_assoc). rewrite ((FZpZ _ Hp).(F_R).(Rmul_comm) p1). rewrite (FZpZ _ Hp).(Finv_l); auto. rewrite (FZpZ _ Hp).(F_R).(Rmul_comm). rewrite (FZpZ _ Hp).(F_R).(Rmul_1_l); auto. apply (FZpZ _ Hp).(F_1_neq_0). unfold pkdiv, div, to_p. fold p_pos; set (pp := mkznz p (y mod p) (modz p y)). fold p_pos; set (p1 := mkznz p (1 mod p) (modz p 1)). pattern pp at 1; rewrite <- ((FZpZ _ Hp).(F_R).(Rmul_1_l) pp). unfold one; fold p_pos; fold p1. rewrite ((FZpZ _ Hp).(F_R).(Rmul_comm) p1). rewrite <- (FZpZ _ Hp).(F_R).(Rmul_assoc). rewrite ((FZpZ _ Hp).(F_R).(Rmul_comm) p1). rewrite (FZpZ _ Hp).(Finv_l); auto. rewrite (FZpZ _ Hp).(F_R).(Rmul_comm). rewrite (FZpZ _ Hp).(F_R).(Rmul_1_l); auto. apply (FZpZ _ Hp).(F_1_neq_0). assert(T1 := scal_correct N_lt_2 N_not_div_2 Rp Hp Hp1 _ _ E1 Ni3). rewrite Ha1 in T1; simpl fst in T1. match type of T1 with equiv _ ?X => set (p1 := X); fold p1 in T1 end. assert(T2 := scal_correct N_lt_2 N_not_div_2 Rp Hp Hp1 _ _ T1 Ni2). rewrite Ha2 in T2; simpl fst in T2. pose (ppG := pG A B N_not_div_2 Rp Hp Hp1). assert (F1: forall p1, List.In p1 (FGroup.s ppG)). intros p2. apply (FELLK_in pell _ (in_all_znz _ p_pos)). assert (F2 := fun u => @scalL_not_1 N A B N_lt_2 N_not_div_2 Rp _ Hp Hp1 R1 sc2 _ _ u T2 Ni1). fold ppG in F2. assert (F3 := @scalL_1 N A B N_lt_2 N_not_div_2 Rp _ Hp Hp1 R1 sc2 _ _ T2 Ni1). fold ppG in F3. rewrite <- psplit_correct in lR_big. rewrite HS1 in lR_big; simpl fst in lR_big; simpl snd in lR_big. assert (E2: e_order (ceqb pell) p1 ppG = (Zmullp lR)). apply order_div; auto. red; simpl; auto. intros z1 Hz1 Hz2. assert (E2: Zpos (z2p z1) = z1). generalize Hz1; case z1; simpl; auto; try (intros p2 HH || intro HH). case not_prime_0; auto. generalize (prime_ge_2 _ HH); unfold Z.le; simpl; intros HH1; case HH1; auto. rewrite <- psplit_correct. rewrite HS1; simpl fst; simpl snd. assert (Hl: List.In (z2p z1) R1). change R1 with (snd (S1, R1)). rewrite <- HS1. apply psplit_prime; auto. rewrite E2; auto. rewrite E2; auto. rewrite Zpos_mult_morphism. rewrite (Zmull_div (z2p z1)); auto. rewrite E2; rewrite Zmult_assoc. assert (Hpz1: z1 > 0). apply Z.lt_gt; apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. red; auto. rewrite Z_div_mult; auto. rewrite gpow_gpow. rewrite <- E2; apply F2; auto. apply (FELLK_in pell _ (in_all_znz _ p_pos)); auto. red; simpl; intros HH; discriminate. apply Z_div_pos; auto with zarith. rewrite Hsc3 in F3; simpl fst in F3. rewrite <- psplit_correct. rewrite HS1; simpl fst; simpl snd. rewrite Zpos_mult_morphism; rewrite gpow_gpow; auto. set (p2 := gpow (gpow p1 ppG S1) ppG (Zmull R1)). fold p2 in F3; inversion F3; auto. red; simpl; intros; discriminate. red; simpl; intros; discriminate. absurd (e_order(ceqb pell) p1 ppG <= (FGroup.g_order ppG)). apply Zlt_not_le. apply Z.le_lt_trans with (1 := gorder_pG A B N_not_div_2 Rp Hp Hp1). rewrite E2. replace (Zpos (Zmullp lR)) with ((Zmullp lR - 1) + 1)%Z; try ring. apply Zplus_lt_compat_r. apply Zlt_square_simpl. change 0 with (1-1). unfold Zminus; apply Zplus_le_compat_r. case Zmullp; try intros p1; red; simpl; intros; discriminate. apply Z.le_lt_trans with (4 * N). replace (2 * p * (2 * p))%Z with (4 * (p * p))%Z. auto with zarith. ring. rewrite <- psplit_correct; rewrite HS1; simpl fst; simpl snd; auto. assert (tmp: forall x, x ^2 = x * x). intros x1; replace 2 with (1 + 1); auto; rewrite Zpower_exp. rewrite Zpower_1_r; auto. red; simpl; intros; discriminate. red; simpl; intros; discriminate. rewrite <- tmp; auto. apply Zdivide_le; auto. apply Zlt_le_weak. apply e_order_pos; auto. apply FGroup.g_order_pos. apply e_order_divide_g_order; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod