proposition: Lemma take_cons_pos : forall x l n, (n > 0) -> take n (x::l) = x :: (take (n-1) l).
proof: Proof. Proof using. introv H. destruct n. false; math. rewrite take_cons. fequals_rec. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)