proposition: Lemma encode_decrease n m l : (length l <= n)%nat -> unique l -> (lmax l < m)%nat -> decrease (encode l n) m.
proof: Proof. revert m l; elim n; simpl; clear n. now intros m l; case l; simpl; auto; clear l. intros n Hrec m l; case l; simpl; auto; clear l. intros p l H1 H2 H3. inversion_clear H2 as [ | xx yy Ha Hb]. split; auto. now apply Nat.le_lt_trans with (2:= H3); apply Nat.le_max_l. generalize H1 H3 Ha Hb; case l; clear l H1 H3 Ha Hb. now intros; case n; simpl; auto. intros c l H1 H3 Ha Hb. apply Hrec; auto. - rewrite encode_aux_length; auto with arith. - apply encode_aux_unique; auto. apply uniqC; auto. - case (Nat.le_gt_cases (c2N p) (lmax (c :: l))); intros H4. rewrite Nat.max_r in H3; auto with zarith. apply Nat.lt_le_trans with (lmax (c :: l)). apply encode_aux_lmax_lt; auto with arith. now intros HH; discriminate. now apply uniqC; auto. now generalize H3; case m; auto with arith. rewrite encode_aux_id; auto. apply Nat.lt_le_trans with (1 := H4). apply Nat.le_trans with (Nat.max (c2N p) (lmax (c :: l))). now apply Nat.le_max_l. generalize H3; case m; auto with arith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max