proposition: Lemma realDed x y : (0%dE >=< x)%O -> (0%dE >=< y)%O -> (0%dE >=< x + y)%O.
proof: Proof. case: x y => [x||] [y||] //; exact: realD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed