proposition: Lemma max_var_correct : forall p j v, In v (vars j p) -> Pos.le v (max_var j p).
proof: Proof. intros p; induction p; simpl. - tauto. - auto. - intros j v H. rewrite in_app_iff in H. destruct H as [H |[ H | H]]. + subst. apply Pos.max_case_strong;intros ; auto. * apply max_var_le. * eapply Pos.le_trans ; eauto. apply max_var_le. + apply Pos.max_case_strong;intros ; auto. eapply Pos.le_trans ; eauto. + apply Pos.max_case_strong;intros ; auto. 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