proposition: Theorem nth_option_Some_lt : forall (A : Set)(ls : list A) i a, nth_option ls i = Some a -> i < length ls.
proof: Proof. induction ls; intuition; simpl in *. discriminate. destruct i. lia. apply ->Nat.succ_lt_mono. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation