proposition: Lemma one_less2lex : forall l l', one_less r l l' -> lex l l'.
proof: Proof. intros l l' H1; inversion H1; subst. generalize dependent l; induction p as [ | p]; intros l Hl H1. destruct l as [|h l]; inversion H1. subst; simpl; constructor; trivial. destruct l as [|h l]; inversion H1. subst; simpl; constructor 2; trivial. apply IHp; trivial. apply (@one_less_cons _ r l (l [p := a']) p a a'); trivial. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)