proposition: Lemma fin_num_doppeB x y : y \is a fin_num -> - (x - y) = - x + y.
proof: Proof. by move=> ?; rewrite doppeB// fin_num_adde_defl// fin_numN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed