fact: Fixpoint list_take {T: Type} i (l: list T) := match i, l with | 0, _ => [] | _, [] => [] | S i, h::t => h :: list_take i t end.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)