proposition: Theorem sn: forall n, 0 <= n -> s (n+1) = (fst (s n) * fst (s n) -2, 0).
proof: Proof. intros n Hn; rewrite sn_aux; generalize (sn_snd n); case (s n); auto. intros x y H; simpl in H; rewrite H; simpl. eq_tac; ring. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup