proposition: Lemma list_max_lt : forall l n, l <> nil -> list_max l < n <-> Forall (fun k => k < n) l.
proof: Proof. intro l; induction l as [|a l IHl]; simpl; intros n Hnil; split; intros H; intuition. - destruct l. + repeat constructor. now simpl in H; rewrite Nat.max_0_r in H. + apply Nat.max_lub_lt_iff in H. now constructor; [ | apply IHl ]. - destruct l; inversion_clear H as [ | ? ? Hlt HF ]. + now simpl; rewrite Nat.max_0_r. + apply IHl in HF. * now apply Nat.max_lub_lt_iff. * intros Heq; inversion Heq. Qed.
imports: PeanoNat