proposition: Lemma encode_aux_lmax_le p l : (lmax (encode_aux l p) <= lmax l)%nat.
proof: Proof. elim l; simpl; auto with zarith. intros a l1 Hrec. generalize (cube_compare_correct p a); case cube_compare; intros H. - apply Nat.max_case; auto with arith. apply Nat.le_trans with (1 := Hrec); auto with arith. - apply Nat.max_case; auto with arith. apply Nat.le_trans with (c2N a); auto with arith. now case a; auto with arith. apply Nat.le_trans with (1 := Hrec); auto with arith. - apply Nat.max_case; auto with arith. apply Nat.le_trans with (1 := Hrec); auto with arith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max