proposition: Lemma subre_ge0 x y : y \is a fin_num -> (0 <= y - x) = (x <= y).
proof: Proof. by move: x y => [x| |] [y| |] //=; rewrite ?(leey, leNye, lee_fin) //= subr_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed