proposition: Lemma lee_dadd a b x y : a <= b -> x <= y -> a + x <= b + y.
proof: Proof. rewrite !dual_addeE leeN2 -leeN2 -(leeN2 y); exact: leeD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed