proposition: Lemma showo : (gen_tag = tt) * (the_tag = tt) * (a_tag = tt).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule