proposition: Theorem firstn_S : forall (A: Type)(defA : A)(n : nat)(ls : list A), n < length ls -> firstn (S n) ls = (firstn n ls) ++ ((nth n ls defA) :: nil).
proof: Proof. induction n; intuition; simpl in *. destruct ls; simpl in *. lia. trivial. destruct ls; simpl in *. lia. f_equal. eapply IHn. lia. Qed.
imports: FCF CompFold