proposition: Lemma encode_aux_in_more l p q : (c2N q >= c2N p)%nat -> ~ (In p l) -> In q (encode_aux l p) -> In (cube_succ q) l.
proof: Proof. intros H1; elim l; simpl; auto with datatypes; clear l. intros p1 l Hrec H2. assert (F0: p1 <> p); auto. assert (F0b: ~ In p l); auto; clear H2. generalize (cube_compare_correct p p1); case cube_compare; intros H3 H4; auto. - case F0; auto. - case H4; clear H4; auto; intros H4. rewrite <- H4; left; generalize H3; case p1; simpl; auto. intros HH; contradict HH; auto with arith. - case H4; clear H4; auto; intros H4. contradict H1; rewrite <- H4; auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik