proposition: Lemma agree_env_tail : forall fr env env', agree_env (Pos.succ fr) env env' -> agree_env fr (Env.tail env) (Env.tail env').
proof: Proof. intros fr env env' H. unfold Env.tail. apply agree_env_jump. rewrite <- Pos.add_1_r in H. apply H. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat