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