proposition: Lemma defaultPoly_mxi_1 n i (H : i < n) : List.In (1%Z, mxi H) (defaultPoly n).
proof: Proof. intros. right. simpl. apply list_of_vec_in. rewrite <- (Vbuild_nth (fun i (ip : i < n) => (1%Z, mxi ip)) H). apply Vnth_in. Qed.
imports: Coq(Program) CoLoR(ListUtil LogicUtil ZUtil VecUtil Problem ATrs SN APolyInt Polynom RelUtil MonotonePolynom PositivePolynom NaryFunction MonAlgChecker IntBasedChecker Proof OptUtil AWFMInterpretation)