proposition: Lemma maxvar_rules_remove : forall a R x y, x >= y -> fold_left fold_max R x >= fold_left fold_max (remove a R) y.
proof: Proof. induction R; simpl; intros. hyp. case (rule_dec a0 a); intro. subst a0. apply IHR. trans x. apply Nat.le_max_l. hyp. simpl. apply IHR. apply max_ge_compat. hyp. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)