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