proposition: Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
proof: Proof. by move=> [r| |] [s| |]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed