proposition: Lemma fine_eq0 x : x \is a fin_num -> (fine x == 0%R) = (x == 0).
proof: Proof. by move: x => [//| |] /=; rewrite fin_numE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed