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