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