proposition: Lemma agree_env_eval_nformula : forall env env' e (AGREE : agree_env (max_var xH (fst e)) env env'), eval_nformula env e <-> eval_nformula env' e.
proof: Proof. intros env env' e; destruct e as [p o]. simpl; intros AGREE. assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p) = (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H. { revert env env' AGREE. generalize xH. induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros p1 **. apply (IHp p1). apply agree_env_jump. eapply agree_env_subset; eauto. rewrite (Pos.add_comm p). rewrite max_var_acc. apply Pos.le_refl. - intros p ? ? AGREE. f_equal;[f_equal|]. + apply (IHp1 p). eapply agree_env_subset; eauto. apply Pos.le_max_l. + f_equal. unfold Env.hd. unfold Env.nth. apply AGREE. apply Pos.le_1_l. + apply (IHp2 p). apply agree_env_tail. eapply agree_env_subset; eauto. rewrite !Pplus_one_succ_r. rewrite max_var_acc. apply Pos.le_max_r. } rewrite H. tauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat