proposition: Lemma fin_numP x : reflect ((x != -oo) /\ (x != +oo)) (x \is a fin_num).
proof: Proof. by apply/(iffP idP) => [/andP//|/andP]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed