proposition: Lemma equiv_refl F (f : T -> V) : f ~_F f.
proof: Proof. by apply/eqaddoP; rewrite subrr. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule