proposition: Lemma maxl_prop : forall nats n, LIn n nats -> n <= maxl nats.
proof: Proof. induction nats; simpl; sp; subst. apply max_prop1. allapply IHnats. assert (maxl nats <= max a (maxl nats)) by apply max_prop2. omega. Qed.
imports: UsefulTypes bin_rels Omega