proposition: Theorem maxList_correct : forall (ls : list nat) n, In n ls -> maxList ls >= n.
proof: Proof. intuition. eapply maxList_correct_h. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation