fact: Fixpoint trunc (v : list A) : nat -> list A := fun n : nat => match v return (list A) with | nil => nil | b :: w => match n return (list A) with | O => nil | S p => b :: trunc w p end end.
imports: Arith_compl Minus Lists_compl