proposition: Theorem sn_snd: forall n, snd (s n) = 0.
proof: Proof. intros n; case n; simpl; auto. intros p; pattern p; apply Pind; auto. intros p1 H; rewrite Zpos_succ_morphism; unfold Z.succ. rewrite sn_aux; auto with zarith. generalize H; case (s (Zpos p1)); simpl. intros x y H1; rewrite H1; auto with zarith. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup