proposition: Lemma lee_subl_addl x y z : y \is a fin_num -> (x - y <= z) = (x <= y + z).
proof: Proof. by move=> ?; rewrite lee_subl_addr// addeC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed