proposition: Lemma maxvar_rules_init_mon : forall R x y, x >= y -> fold_left fold_max R x >= fold_left fold_max R y.
proof: Proof. induction R; simpl; intros. hyp. apply IHR. unfold fold_max. apply max_ge_compat. hyp. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)