proposition: Lemma drop_nth_length : forall l p, length (drop_nth l p) >= pred (length l).
proof: Proof. intros. destruct (le_gt_dec (length l) p). rewrite drop_nth_beyond; trivial. lia. rewrite drop_nth_in_length; auto. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)