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