proposition: Lemma incl_lmax : forall l1 l2, incl l1 l2 -> lmax l1 <= lmax l2.
proof: Proof. intros l1 l2. induction l1 as [| a' l' Hrec]. auto with arith. intro H. gen (incl_cons_l H). clear H. intros (H1, H2). simpl. apply (Nat.max_case a' (lmax l') (fun n : nat => n <= lmax l2)). apply in_lmax. hyp. apply Hrec. hyp. Qed.
imports: CoLoR(ListUtil LogicUtil NatUtil)