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