proposition: Lemma cvg_prod T {U U' V V' : filteredType T} (x : U) (l : U') (y : V) (k : V') : x --> l -> y --> k -> (x, y) --> (l, k).
proof: Proof. move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=. split; [exact: xl | exact: yk]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed