proposition: Lemma take_app_drop_spec : forall n l f r, f = take n l -> r = drop n l -> n <= length l -> l = f ++ r /\ length f = n /\ length r = length l - n.
proof: Proof. Proof using. intros n. induction n; introv F R L. { subst. rew_listx. splits~. math. } { destruct l; rew_listx in L. { rew_listx in L. false. math. } { forwards~ (F'&R'&L'): (>> IHn l (take n l) r). { math. } subst f. rew_listx. splits. { fequals. } { math. } { math. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)