Proved plus_lt theorem from MoreProp.