proposition: Lemma drop_is_suffix : forall n l, exists q, l = q ++ drop n l.
proof: Proof. Proof using. intros n l. gen n. induction l; intros. { exists (@nil A). rewrite~ drop_nil. } { destruct n as [|n']. { rewrite drop_zero. exists~ (@nil A). } { rewrite drop_succ. forwards (q'&E): IHl n'. exists (a::q'). rew_list. congruence. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)