# Library AuxLib

``` Require Import List. Require Import Max. Require Import Omega. ```
 Notations for lists.
``` Bind Scope list_scope with list. Arguments Scope app [type_scope list_scope list_scope]. Arguments Scope cons [type_scope _ list_scope]. Arguments Scope List.In [type_scope _ list_scope]. Infix "::" := cons (at level 60, right associativity) : list_scope. Infix "++" := app (right associativity, at level 60) : list_scope. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope. ```
 List membership theorems.
``` Lemma list_not_in_cons_l :   forall (A : Type) (x : A) y M, {x = y} + {x <> y} -> ~ In x (y :: M) -> x <> y. ```
``` Lemma max_lt_l :   forall (x y z : nat), x <= y -> x <= max y z. Hint Resolve max_lt_l : arith. Lemma max_lt_r :   forall (x y z : nat), x <= z -> x <= max y z. Hint Resolve max_lt_r : arith. Lemma le_lt_S :   forall (n m : nat),   n <= m -> n < S m. Hint Resolve le_lt_S : arith. Lemma lt_Sn_n :   forall (n m : nat),   n < S m -> n <> m -> n < m. Hint Resolve lt_Sn_n : arith. Lemma finite_nat_list_max :   forall (l : list nat),   { n : nat | forall x, In x l -> x <= n }. Lemma finite_nat_list_max' :   forall (l : list nat),   { n : nat | ~ In n l }. ```