proposition: Lemma adde_Neq_pinfty 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