proposition: Lemma drop_app_r : forall n l l', (n >= length l) -> drop n (l ++ l') = drop (n - length l) l'.
proof: Proof. Proof using. induction n; destruct l; introv H; rew_list in *; auto. { false. math. } { rewrite drop_cons. rewrite IHn. fequals. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)