fact: Fixpoint vars (jmp : positive) (p : Pol Z) : list positive := match p with | Pc c => nil | Pinj j p => vars (Pos.add j jmp) p | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory