proposition: Lemma solve_length s : valid_state s -> length (solve s) <= 11.
proof: Proof. intro Hs. assert (tmp: forall a b c, a = b -> a <= c -> b <= c). now intros a b c H1 H2; rewrite <- H1; auto. apply tmp with (length (tc2_solve 11 s s1 s2)). apply f_equal with (f := @length _). now apply sym_equal; exact (solve_eq s). apply tc2_solve_length. now exact s12. exact Hs. Qed.
imports: Int31 List BasicRubik Rubik31