proposition: Lemma length_take : forall n l, n <= length l -> length (take n l) = n.
proof: Proof. Proof using. introv E. forwards~ (l'&N&M): take_spec n l. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)