proposition: Lemma agree_env_jump : forall fr j env env', agree_env (fr + j) env env' -> agree_env fr (Env.jump j env) (Env.jump j env').
proof: Proof. intros fr j env env' H. unfold agree_env ; intro. intros. unfold Env.jump. apply H. apply Pos.add_le_mono_r; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat