proposition: Lemma fold_left_max_ge_init : forall (ls : list nat)(n : nat), fold_left max ls n >= n.
proof: Proof. induction ls; intuition; simpl in *. eapply Nat.le_trans. eapply Nat.max_lub_l. eapply Nat.le_refl. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation