proposition: Theorem sn_w: forall n, 0 <= n -> ppow w (2 ^ (n + 1)) = pplus (pmult (s n) (ppow w (2 ^ n))) (- 1, 0).
proof: Proof. intros n H; unfold s; simpl; rewrite Zpower_exp; auto with zarith. assert (Hu: 0 <= 2 ^n); auto with zarith. rewrite Zpower_1_r; rewrite ppow_ppow; auto with zarith. repeat rewrite pplus_pmult_dist_r || rewrite pplus_pmult_dist_l. pattern 2 at 2; replace 2 with (1 + 1); auto with zarith. rewrite ppow_add; auto with zarith; simpl. rewrite pmult_1_r; auto. repeat rewrite <- ppow_mult; auto with zarith. rewrite (pmult_comm v w); rewrite w_mult_v. rewrite ppow_1; simpl. 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