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.
| Facts about arithmetic. |
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 }.