proposition: Lemma nth_option_not_None : forall (A : Set)(ls : list A)(i : nat), i < length ls -> nth_option ls i = None -> False.
proof: Proof. induction ls; intuition; simpl in *. lia. destruct i. discriminate. assert (i < length ls). lia. eauto. Qed.
imports: FCF.FCF