proposition: Theorem lsAppCons : forall (A : Type)(ls : list A)(n : nat)(def : A), n < length ls -> ls = (firstn n ls) ++ ((nth n ls def) :: (skipn (S n) ls)).
proof: Proof. induction ls; destruct n; intuition idtac; simpl in *. lia. lia. f_equal. eapply IHls. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation