proposition: Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
proof: Proof. by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed