proposition: Lemma decode_aux_app p l1 l2 : decode_aux (l1 ++ l2) p = decode_aux l1 p ++ decode_aux l2 p.
proof: Proof. revert l2; elim l1; simpl; auto. intros a l3 Hrec; case cube_compare; intros l2; rewrite Hrec; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik