proposition: Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) : Signed.spec 0 nz cond x%:num%:E.
proof: Proof. apply/andP; split. case: cond nz x => [[[]|]|] [] x //=; do ?[by case: (bottom x)|by rewrite eqe eq0F]. case: cond nz x => [[[]|]|] [] x //=; do ?[by case: (bottom x)|by rewrite ?lee_fin ?(eq0, ge0, le0) ?[_ || _]cmp0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed