proposition: Theorem skipn_S : forall (A: Type)(defA : A)(ls : list A)(n : nat), n < length ls -> skipn n ls = nth n ls defA :: skipn (S n) ls.
proof: Proof. induction ls; intuition; simpl in *. destruct n; try lia. destruct n. simpl. trivial. simpl. eapply IHls. lia. Qed.
imports: FCF CompFold