proposition: Lemma max_var_le : forall p v, (v <= max_var v p)%positive.
proof: Proof. intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - intros. apply Pos.le_refl. - intros v. specialize (IHp (p+v)%positive). eapply Pos.le_trans ; eauto. assert (xH + v <= p + v)%positive. { apply Pos.add_le_mono. - apply Pos.le_1_l. - apply Pos.le_refl. } eapply Pos.le_trans ; eauto. apply pos_le_add. - intros v. apply Pos.max_case_strong;intros ; auto. specialize (IHp2 (Pos.succ v)%positive). eapply Pos.le_trans ; eauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory