fact: Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := match p with | Pc _ => jmp | Pinj j p => max_var (Pos.add j jmp) p | PX p j q => Pos.max (max_var jmp p) (max_var (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