proposition: Theorem nth_error_not_None : forall (ls : list A)(n : nat), n < length ls -> nth_error ls n = None -> False.
proof: Proof. induction ls; destruct n; intuition; simpl in *. lia. lia. inversion H0. eapply IHls; eauto. lia. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation