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