proposition: Lemma lmax_app l1 l2 : lmax (l1 ++ l2) = Nat.max (lmax l1) (lmax l2).
proof: Proof. revert l2; elim l1; simpl; clear l1; auto. intros a l Hrec l2. rewrite <- Nat.max_assoc; rewrite Hrec; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max