proposition: Lemma naive_auxC m p c l1 l2 a b : naive_int63it_aux _ (fun s l1 l2 p => s ++ (l1,l2,p) :: nil) m p c l1 l2 (a :: b) = a :: naive_int63it_aux _ (fun s l1 l2 p => s ++ (l1,l2,p) :: nil) m p c l1 l2 b.
proof: Proof. revert p c l1 l2 a b; elim m; clear m. - intros p c l1 l2 a b; repeat rewrite naive_aux0. case int63i; auto. - intros m Hrec p c l1 l2 a b. repeat rewrite naive_auxS. case int63i; simpl; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik