proposition: Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).
proof: Proof. by rewrite fin_numE negb_and ?negbK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed