proposition: Lemma take_cons_case : forall x l n, n >= 0 -> take n (x::l) = If n = 0 then nil else x :: (take (n-1) l).
proof: Proof. Proof using. introv Hn. case_if. { subst. applys take_zero. } { applys* take_cons_pos. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)