proposition: Lemma drop_is_suffix : forall n l, exists q, l = q ++ drop n l.
proof: Proof. Proof using. intros. unfold drop. apply LibList.drop_is_suffix. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)