proposition: Lemma mseq_lift_right_left : forall (O:ord) (f:natO -m> O) n, mseq_lift_left f n == mseq_lift_right f n.
proof: Proof. intros; apply fmon_eq_intro; unfold mseq_lift_left,mseq_lift_right; simpl; intros. replace (n0+n)%nat with (n+n0)%nat; auto with arith. Qed.