proposition: Lemma ltR_subl_addr x y z : (x - y < z) <-> (x < z + y).
proof: Proof. split => H; [apply (@ltR_add2r (-y)) | apply (@ltR_add2r y)]; last by rewrite subRK. by rewrite -addRA; apply: (ltR_leR_trans H); rewrite Rplus_opp_r addR0; exact/Rle_refl. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)