proposition: Lemma equiv_sym F (f g : T -> V) : f ~_F g -> g ~_F f.
proof: Proof. move=> fg; have /(canLR (addrK _))<- := fg. by apply:eqaddoE; rewrite oppo (equivoRL _ fg). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule