proposition: Lemma naive_auxA a1 a2 m p c l1 l2 : naive_int63it_aux _ (fun s l1 l2 p => s ++ (l1,l2,p) :: nil) m p c l1 l2 (a1 ++ a2) = a1 ++ naive_int63it_aux _ (fun s l1 l2 p => s ++ (l1,l2,p) :: nil) m p c l1 l2 a2.
proof: Proof. elim a1; clear a1; auto. intros hd a1 Hrec. simpl; rewrite naive_auxC; apply f_equal2 with (f := @cons _); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik