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