fact: Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := match p as p return p <= n -> t A p with | 0 => fun _ => [] | S p' => match v in t _ n return S p' <= n -> t A (S p') with | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le) | x::xs => fun le => x::take p' (le_S_n p' _ le) xs end end le.
imports: Arith_base