proposition: Lemma max_var_acc : forall p i j, (max_var (i + j) p = max_var i p + j)%positive.
proof: Proof. intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros. rewrite ! IHp. rewrite Pos.add_assoc. reflexivity. - intros. rewrite !Pplus_one_succ_l. rewrite ! IHp1. rewrite ! IHp2. rewrite ! Pos.add_assoc. rewrite <- Pos.add_max_distr_r. reflexivity. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat