proposition: Lemma iter_final n : let (s1,s2) := iter n in match s2 with OTC2 => forall s, reachable s -> nlreachable (Nat.pred n) s | _ => True end.
proof: Proof. generalize (iter_equiv n) (iters_final n). case (iters n); case (iter n). intros s1 s2; case s2; auto. intros l1 l2; case l2; auto. intros s l3 [_ H1]. generalize (H1 (rev3 (encode_state s))). simpl tc2it; rewrite in_map_iff; intros [_ H2]. case H2; exists s; simpl; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max