proposition: Lemma encode_aux_unique p l : unique (p :: l) -> unique (encode_aux l p).
proof: Proof. generalize p; elim l; simpl; auto; clear p l. now intros; apply uniqN. intros q l Hrec1 p Hpal. inversion_clear Hpal as [ | xx yy Ha Hl]. inversion_clear Ha as [ | xx yy Ha1 Hl1]. apply uniqC. apply Hrec1; auto. now apply uniqC; auto with datatypes. generalize (cube_compare_correct p q); case cube_compare; intros H1 H2. - case Hl; rewrite H1; auto with datatypes. - case Hl1. replace q with (cube_succ (cube_pred q)). apply encode_aux_in_more with p; auto with datatypes. now generalize H1; case p; case q; simpl; auto with arith. generalize H1; case q; auto; intros HH; contradict HH; auto with arith. - case Hl1; apply encode_aux_in_less with p; auto with zarith datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik