proposition: Lemma ltM_trans_1 : forall a b l l' l'', a < b -> ltM a l l' -> ltM b l' l'' -> ltM b l l''.
proof: Proof. destruct 2. destruct 1. split. replace (multiplicity b l) with (multiplicity b l'). auto. symmetry;apply H1; auto. intros; transitivity (multiplicity b0 l');auto. apply H1. eapply lt_trans; eauto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0