proposition: Lemma nonneg_plus_lt_compat_r x y z : 0 ≤ z -> x < y -> x < y + z.
proof: Proof. intros. rewrite <-(plus_0_r x). apply plus_lt_le_compat;trivial. Qed.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps