proposition: Lemma cvg_trans T (G F H : set_system T) : (F `=>` G) -> (G `=>` H) -> (F `=>` H).
proof: Proof. by move=> FG GH P /GH /FG. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed