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