proposition: Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
proof: Proof. rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed