proposition: Theorem skipn_nil_impl_short : forall (A : Type)(n : nat)(ls : list A), skipn n ls = nil -> (length ls <= n)%nat.
proof: Proof. induction n; destruct ls; intuition idtac; simpl in *. lia. discriminate. lia. eapply le_n_S. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation