proposition: Lemma in_lmax : forall x l, In x l -> x <= lmax l.
proof: Proof. induction l; simpl; intro. contr. destruct H. subst a. apply Nat.le_max_l. ded (IHl H). apply le_max_intro_r. exact H0. Qed.
imports: CoLoR(ListUtil LogicUtil NatUtil)