proposition: Lemma drop_app_length : forall l l', drop (length l) (l ++ l') = l'.
proof: Proof. Proof using. intros. rewrite drop_app_r; [|math]. math_rewrite (forall a, a - a = 0). rewrite drop_zero. rew_list~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)