proposition: Lemma dual_addeE x y : (x + y)%dE = - ((- x) + (- y))%E.
proof: Proof. by case: x => [x| |]; case: y => [y| |] //=; rewrite opprD !opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed