proposition: Lemma maxList_correct_h : forall (ls : list nat)(n init : nat), In n ls -> fold_left max ls init >= n.
proof: Proof. induction ls; intuition. inversion H. simpl in *. intuition; subst. eapply Nat.le_trans. eapply Nat.max_lub_r. eapply Nat.le_refl. eapply fold_left_max_ge_init. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation