proposition: Lemma tc2_get_next_movel s l1 l2 : match tc2_get_next s l1 l2 with Some m => In m Movel | _ => True end.
proof: Proof. unfold tc2_get_next. elim Movel; simpl; auto. intros a l Hrec; case positive_eq; auto. generalize Hrec; case tc2_get_next_aux; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max