proposition: Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) (x : {compare (0 : \bar R) & xnz & xr}) : Signed.spec 0%R ?=0 xr (fine x%:num).
proof: Proof. case: xr x => [[[]|]|]//= [x /andP[_]]/=. - by move=> /eqP ->. - by case: x. - by case: x. - by move=> /orP[]; case: x => [x||]//=; rewrite lee_fin => ->; rewrite ?orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed