proposition: Lemma monotonic_lt : forall f ss ts, one_less lt ss ts -> lt (Fun f ss) (Fun f ts).
proof: Proof. assert (leF_po : preorder Sig leF). apply leF_preorder. intros f ss ts Hol. apply lt_status. elim (leF_po); intros leF_refl leF_trans. split; apply leF_refl. intros s s_in_ss. inversion Hol; subst. elim (in_exists_element_at s_in_ss); intros p' Hp'. elim (eq_nat_dec p p'); intro case_p_p'. subst p'; rewrite H0 in Hp'. inversion Hp'; subst. apply lt_subterm. exists a'; split; trivial. apply exists_element_at_in. exists p; apply element_at_replaced. elim (@element_at_exists _ ss p); intros H1 H2. apply H2; exists s; trivial. right; hyp. apply lt_subterm. exists s; split. apply exists_element_at_in. exists p'; rewrite <- (@element_at_not_replaced _ ss p' p); trivial. intro; elim case_p_p'; subst; trivial. left; trivial. apply mono_axiom; hyp. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)