proposition: Lemma pi_compat_rule_weak : forall r, coef_pos (rulePoly_ge r) -> succ_eq (lhs r) (rhs r).
proof: Proof. intros r H_coef_pos. unfold succ_eq, IR. intro xint. unfold Dge, Dle, 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)), !val_peval_D. apply pos_le. rewrite <- peval_minus. 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)