proposition: Lemma encode_aux_id p l : (lmax l < c2N p -> encode_aux l p = l)%nat.
proof: Proof. elim l; simpl; auto. intros a l1 Hrec Hp. assert (Hp1: (lmax l1 < c2N p)%nat). now apply Nat.le_lt_trans with (2 := Hp); auto with arith. assert (Hp2: (c2N a < c2N p)%nat). now apply Nat.le_lt_trans with (2 := Hp); auto with arith. generalize (cube_compare_correct p a); case cube_compare; intros H1. - apply f_equal2 with (f := @cons _); auto. - contradict H1; auto with zarith. - apply f_equal2 with (f := @cons _); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max