proposition: Lemma encode_aux_lmax_lt l p : (l <> nil -> unique (p :: l) -> c2N p <= lmax l -> lmax (encode_aux l p) < lmax l)%nat.
proof: Proof. revert l p. assert (F0 : forall p l, l <> nil -> unique (p :: l) -> (c2N p <= lmax l -> c2N p < lmax l)%nat). intros p l Hl H H1; apply Nat.lt_eq_cases in H1; destruct H1 as [H2|H2]; auto. case (lmax_inv l); auto. intros q; rewrite <- H2; intros (H3, H4). inversion_clear H as [ | xx yy Ha Hb]. case Hb; replace p with q; auto. now generalize H3; case p; case q; auto; intros; discriminate. intros l; elim l; simpl. now intros p HH; case HH; auto. intros a l1 Hrec p _ Hp. generalize (cube_compare_correct p a); case cube_compare; intros Hp1 H1. - inversion_clear Hp as [ | xx yy Ha Hb]. case Hb; rewrite Hp1; auto with datatypes. - apply Nat.max_case; auto. apply Nat.lt_le_trans with (c2N a); auto with arith. now generalize Hp1; case a; auto with arith; intros HH; contradict HH; auto with arith. generalize Hrec Hp H1 ; case l1; auto; clear l1 Hrec Hp H1. simpl lmax; generalize Hp1; case a; simpl; auto with arith. now intros HH; contradict HH; auto with arith. intros a1 l2 Hrec Hp H1. case (Nat.le_gt_cases (c2N p) (lmax (a1 :: l2))); intros H2. apply Nat.lt_le_trans with (lmax (a1 :: l2)); auto with arith. apply Hrec; auto; try (intros; discriminate). inversion_clear Hp as [ | xx yy Ha Hb]. inversion_clear Ha as [ | xx1 yy1 Ha1 Hb1]. now apply uniqC; auto with datatypes. apply Nat.lt_le_trans with (c2N a); auto with arith. apply Nat.le_lt_trans with (c2N p); auto with arith. apply Nat.le_trans with (lmax (a1 :: l2)); auto with arith. apply encode_aux_lmax_le; auto. - assert (H2: (c2N p <= (lmax l1))%nat). now generalize H1 Hp1; apply Nat.max_case; auto with zarith. generalize Hrec Hp H2 ; case l1; auto; clear l1 Hrec Hp H1 H2. simpl lmax. now intros _ _ HH; contradict HH; auto with zarith. intros a1 l2 Hrec Hp H1. rewrite (Nat.max_r (c2N a) (lmax (a1 :: l2))); auto with zarith. apply Nat.max_case; auto with zarith. apply Hrec; auto with arith; try (intros; discriminate). inversion_clear Hp as [ | xx yy Ha Hb]. inversion_clear Ha as [ | xx1 yy1 Ha1 Hb1]. apply uniqC; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max