proposition: Lemma leR_subr_addr x y z : (x <= y - z) <-> (x + z <= y).
proof: Proof. split => [|H]. by move=> /RleP; rewrite RminusE lerBrDr => /RleP. by apply/RleP; rewrite RminusE lerBrDr; exact/RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)