proposition: Lemma equivalence_rel_equiv F : equivalence_rel [rel f g : T -> V | f ~~_F g].
proof: Proof. move=> f g h; split; first by apply/eqP/equiv_refl. by move=> /eqP fg /=; apply/eqP/eqP; apply/equiv_trans => //; apply/equiv_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule