proposition: Lemma fin_numPn x : reflect (x = -oo \/ x = +oo) (x \isn't a fin_num).
proof: Proof. by rewrite fin_numEn; apply: (iffP orP) => -[]/eqP; by [left|right]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed