proposition: Lemma encode_aux_in_less l p q : (c2N q < c2N p)%nat -> ~(In p l) -> In q (encode_aux l p) -> In q l.
proof: Proof. intros H1; elim l; simpl; auto with datatypes; clear l. intros p1 l Hrec H2. generalize (cube_compare_correct p p1); case cube_compare; intros HH; auto. - case H2; auto. - intros [HH1 | HH1]; auto. assert (H: (c2N q + 1 = c2N p1)%nat). now generalize HH HH1; case p1; case q; simpl; auto; try (intros; discriminate); intros HH2; contradict HH2; auto with arith. intros; apply False_ind; auto with zarith. right; apply Hrec; auto. - intros [HH1 | HH1]; auto. right; apply Hrec; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik