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