proposition: Theorem skipn_lt_nil_false : forall (A : Type)(ls : list A)(n : nat), n < length ls -> skipn n ls = nil -> False.
proof: Proof. induction ls; intuition; simpl in *. lia. destruct n; simpl in *; intuition. discriminate. eapply IHls; eauto. lia. Qed.
imports: FCF.FCF FCF.CompFold