proposition: Lemma tc2_solve_length n s s1 s2 : (s1, s2) = fst (iter2 n) -> valid_state s -> (length (tc2_solve n s s1 s2) <= n)%nat.
proof: Proof. intros H1 H. rewrite <- (tc2_solve_equiv n s (fst (fst (iter2s n))) (snd (fst (iter2s n))) s1 s2); auto. - apply solve_length; auto. - generalize (iter2s_valid n). intros (HH1, HH2); auto. - rewrite H1; case (iter2_equiv n); intros HH (HH1, _); split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max