proposition: Lemma ltM_appR : forall a l l' l'', ltM a l l' -> ltM a (app l l'') (app l' l'').
proof: Proof. intros. eapply ltM_equiv_ltM. 2:apply app_equiv_comm. eapply ltM_equiv_ltMR. 2:apply app_equiv_comm. apply ltM_app. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0