proposition: Theorem nth_option_None_ge : forall (A : Set)(ls : list A) i, nth_option ls i = None -> i >= length ls.
proof: Proof. induction ls; intuition; simpl in *. destruct i. discriminate. eapply le_n_S. eapply IHls. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation