proposition: Lemma lerB x y z t : x <= y -> t <= z -> x - z <= y - t.
proof: Proof. by move=> lxy ltz; rewrite lerD // lterN2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)