proposition: Lemma dfineD : {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