proposition: Lemma Rle_up a : a <= IZR (Z.abs (up a)).
proof: Proof. case: (Rlt_le_dec a 0) => Ha; last by apply Rle_up_pos. apply (@leR_trans 0); first Lra.lra. exact/IZR_le/Zabs_pos. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)