proposition: Lemma eqe_oppLRP x y : (- x = y) <-> (x = - y).
proof: Proof. split=> /eqP; first by rewrite eqe_oppLR => /eqP. by rewrite -eqe_oppLR => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed