fact: Definition tree_of (T : nat -> pointedType) : pseudoMetricType R := [the pseudoMetricType R of prod_topology (fun n => pointed_discrete_topology (T n))].
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum interval rat) mathcomp(finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) reals signed topology HB(structures)