proposition: Theorem SS_prop: forall n, 1 < n -> SS n = fst(s (n -2)) mod (Mp n).
proof: Proof. intros n Hn; unfold SS. cut (0 <= n - 2); auto with zarith. case (n - 2). intros _; rewrite Zmodd_correct; rewrite s0; auto. intros p1 H2; rewrite SS_aux_correct with (n := 0); auto with zarith. apply Z.le_lt_trans with 1; try apply mersenne_pos; auto with zarith. rewrite Zmodd_correct; rewrite s0; auto. intros p1 H2; case H2; auto. Qed.
imports: ZArith ZCAux Tactic Wf_nat NatAux UList ListAux FGroup EGroup PGroup IGroup