proposition: Lemma agree_env_subset : forall v1 v2 env env', agree_env v1 env env' -> Pos.le v2 v1 -> agree_env v2 env env'.
proof: Proof. unfold agree_env. intros v1 v2 env env' H ? ? ?. apply H. 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 Wf_nat