proposition: Theorem sn_aux: forall n, 0 <= n -> s (n+1) = (pplus (pmult (s n) (s n)) (-2, 0)).
proof: Proof. intros n Hn. assert (Hu: 0 <= 2 ^n); auto with zarith. set (y := (fst (s n) * fst (s n) - 2, 0)). unfold s; simpl; rewrite Zpower_exp; auto with zarith. rewrite Zpower_1_r; rewrite ppow_ppow; auto with zarith. repeat rewrite pplus_pmult_dist_r || rewrite pplus_pmult_dist_l. repeat rewrite <- pplus_assoc. eq_tac; auto. pattern 2 at 2; replace 2 with (1 + 1); auto with zarith. rewrite ppow_add; auto with zarith; simpl. rewrite pmult_1_r; auto. rewrite Zmult_comm; rewrite ppow_ppow; simpl; auto with zarith. repeat rewrite <- ppow_mult; auto with zarith. rewrite (pmult_comm v w); rewrite w_mult_v. rewrite ppow_1. repeat rewrite tpower_1. rewrite pplus_comm; repeat rewrite <- pplus_assoc; rewrite pplus_comm; repeat rewrite <- pplus_assoc. simpl; case (ppow (7, -4) (2 ^n)); simpl; intros z1 z2; eq_tac; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup