proposition: Lemma adde_Neq_ninfty x y : x != +oo -> y != +oo -> (x + y != -oo) = (x != -oo) && (y != -oo).
proof: Proof. by move: x y => [x| |] [y| |]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed