proposition: Lemma take_cons_pos : forall x l n, (n > 0) -> take n (x::l) = x :: (take (n-1) l).
proof: Proof. Proof using. intros. unfold take. rew_to_nat_nonneg~. rewrite~ LibList.take_cons_pos. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)