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