proposition: Theorem SS_aux_correct: forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 -> iter_pos _ (fun x => Zmodd (Z.square x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1.
proof: Proof. intros p; pattern p; apply Pind. simpl. intros z1 z2 n Hn H H1; rewrite sn; auto; rewrite H1; rewrite Zmodd_correct; rewrite Zsquare_correct; simpl. unfold Zminus; rewrite Zplus_mod; auto. rewrite (Zplus_mod (fst (s n) * fst (s n))); auto with zarith. eq_tac; auto. eq_tac; auto. apply sym_equal; apply Zmult_mod; auto. intros n Rec z1 z2 n1 Hn1 H1 H2. rewrite Pplus_one_succ_l; rewrite iter_pos_plus. rewrite (Rec _ _ n1); auto. replace (n1 + Zpos (1 + n)) with ((n1 + Zpos n) + 1). rewrite sn; simpl; try rewrite Zmodd_correct; try rewrite Zsquare_correct; simpl; auto with zarith. unfold Zminus; rewrite Zplus_mod; auto. unfold Zmodd. rewrite (Zplus_mod (fst (s (n1 + Zpos n)) * fst (s (n1 + Zpos n)))). eq_tac; auto. eq_tac; auto. apply sym_equal; apply Zmult_mod; auto. rewrite Zpos_plus_distr; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup