proposition: Lemma iter2s_final n : let (ss1, s3) := iter2s n in let (s1, s2) := ss1 in match s3 with nil => (forall s, reachable s -> In s s1 \/ In s s2) /\ (forall s, In s s1 -> exists m1, m1 <= n /\ nsreachable m1 s /\ is_odd (porder m1)) /\ (forall s, In s s2 -> exists m1, m1 <= n /\ nsreachable m1 s /\ porder m1 <> 1%positive) | _ => True end.
proof: Proof. generalize (iter2s_correct n). case iter2s; intros (s1, s2) s3. case s3; auto; simpl. intros (H1, (H2, H3)). split; auto. - intros s Hs. case (reachable_nreachable _ Hs). intros k Hk. case (nsreachable_bound _ _ Hk). intros m (Hm, Hm1). case (Nat.le_gt_cases m n); intros Hn. + case (porder_inv1 m); intros H4. * right; rewrite H2; exists m; auto. * left; rewrite H1; exists m; auto. + case (nsreachable_inv n m s); auto with arith. intros s4 Hs3; case (H3 s4). intros HH; case (HH Hs3); auto. - split; auto. + intros s; case (H1 s); auto. + intros s; case (H2 s); auto. Qed.
imports: ZArith List