proposition: Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t.
proof: Proof. rewrite !dual_addeE leeNl oppeK -leeN2 !oppeK; exact: leeD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed