proposition: Lemma leeB x y z u : x <= y -> u <= z -> x - z <= y - u.
proof: Proof. move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//. by rewrite !lee_fin; exact: lerB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed