proposition: Lemma pi_compat_rule : forall r, coef_pos (rulePoly_gt r) -> succ (lhs r) (rhs r).
proof: Proof. intros r H_coef_pos. unfold succ, IR. intro xint. unfold Dgt, Dlt, transp. set (mvl := maxvar (lhs r)). set (mvr := maxvar (rhs r)). rewrite (PI_term_int_eq xint (Nat.le_max_l mvl mvr)), (PI_term_int_eq xint (Nat.le_max_r mvl mvr)). rewrite !val_peval_D. pose (v := (Vmap (proj1_sig (P:=pos)) (vec_of_val xint (S (max mvl mvr))))). apply pos_lt. rewrite <- (peval_const (1)%Z v), <- !peval_minus. unfold v. apply pos_peval. exact H_coef_pos. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)