proposition: Lemma termpoly_v_eq_2 : forall x k (H : (x<=k)%nat) (v : vector Z (S k)), peval (termpoly (BVar H)) v = meval (mxi (NatCompat.gt_le_S (NatCompat.le_lt_n_Sm H))) v.
proof: Proof. intros x k H v. rewrite termpoly_v_eq_1. unfold pzero. unfold peval at 1. ring. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)