proposition: Lemma lmax_inv l : (l <> nil -> exists p, lmax l = c2N p /\ In p l)%nat.
proof: Proof. elim l; simpl. now intros HH; case HH; auto with arith. intros c1 l1; case l1. intros; exists c1; split; simpl; auto. now rewrite Nat.max_l; auto with arith. intros c2 l2 HH; case HH; auto. now intros; discriminate. intros c3 (Hc3, Hc4); rewrite Hc3. apply Nat.max_case. now intros; exists c1; auto. intros; exists c3; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max