fact: Hypothesis refine_invar : forall n U e, tree_invariant U -> tree_invariant (@refine_apx n U e).
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)