proposition: Lemma drop_nth_in_length : forall p l, length l > p -> length (drop_nth l p) = pred (length l).
proof: Proof. induction p; destruct l; auto; intros. unfold drop_nth; simpl. rewrite finalSeg_cons; trivial. change (drop_nth (a :: l) (S p)) with (a :: drop_nth l p). simpl in *; rewrite IHp. destruct l; trivial. simpl in H; lia. lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)