fact: Fixpoint div (p: pol) (x: A) {struct p} : pol * A := match p with nil => (nil, zero) | a::nil => (nil, a) | a::p1 => (snd (div p1 x)::fst (div p1 x), (plus a (mult x (snd (div p1 x))))) end.
imports: ZArith List UList Tactic Permutation