Files

  • mathcomp

    • Top source

    S (Lemmas)

    Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Notations

    S (Lemmas)

    S05_inj [prf, in mathcomp.solvable.burnside_app]
    S0_inv [prf, in mathcomp.solvable.burnside_app]
    S14_inj [prf, in mathcomp.solvable.burnside_app]
    S1_inv [prf, in mathcomp.solvable.burnside_app]
    s23_inv [prf, in mathcomp.solvable.burnside_app]
    S23_inv [prf, in mathcomp.solvable.burnside_app]
    S2_inv [prf, in mathcomp.solvable.burnside_app]
    S3_inv [prf, in mathcomp.solvable.burnside_app]
    S4_inv [prf, in mathcomp.solvable.burnside_app]
    S5_inv [prf, in mathcomp.solvable.burnside_app]
    S6_inv [prf, in mathcomp.solvable.burnside_app]
    same_connect [prf, in mathcomp.boot.fingraph]
    same_connect1 [prf, in mathcomp.boot.fingraph]
    same_connect1r [prf, in mathcomp.boot.fingraph]
    same_connect_r [prf, in mathcomp.boot.fingraph]
    same_connect_rev [prf, in mathcomp.boot.fingraph]
    same_connected_component [prf, in mathcomp.analysis.topology_theory.connected]
    same_fconnect1 [prf, in mathcomp.boot.fingraph]
    same_fconnect1_r [prf, in mathcomp.boot.fingraph]
    same_fconnect_finv [prf, in mathcomp.boot.fingraph]
    same_pblock [prf, in mathcomp.boot.finset]
    same_prefix0 [prf, in mathcomp.classical.classical_orders]
    same_prefix_leq [prf, in mathcomp.classical.classical_orders]
    same_prefix_refl [prf, in mathcomp.classical.classical_orders]
    same_prefix_sym [prf, in mathcomp.classical.classical_orders]
    same_prefix_trans [prf, in mathcomp.classical.classical_orders]
    scalar_mx_block [prf, in mathcomp.algebra.matrix]
    scalar_mx_cent [prf, in mathcomp.algebra.mxalgebra]
    scalar_mx_is_diag [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_monoid_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_scalar [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_trig [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_key [prf, in mathcomp.algebra.matrix]
    scalar_mx_sum_delta [prf, in mathcomp.algebra.matrix]
    scalar_mxC [prf, in mathcomp.algebra.matrix]
    scalar_mxM [prf, in mathcomp.algebra.matrix]
    scale0mx [prf, in mathcomp.algebra.matrix]
    scale1mx [prf, in mathcomp.algebra.matrix]
    scale_0poly [prf, in mathcomp.algebra.poly]
    scale_1poly [prf, in mathcomp.algebra.poly]
    scale_ball0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ball1 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ball_set0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ballE [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_block_mx [prf, in mathcomp.algebra.matrix]
    scale_col_mx [prf, in mathcomp.algebra.matrix]
    scale_lfunE [prf, in mathcomp.algebra.vector]
    scale_poly_eq0 [prf, in mathcomp.algebra.poly]
    scale_poly_key [prf, in mathcomp.algebra.poly]
    scale_polyA [prf, in mathcomp.algebra.poly]
    scale_polyAl [prf, in mathcomp.algebra.poly]
    scale_polyC [prf, in mathcomp.algebra.poly]
    scale_polyDl [prf, in mathcomp.algebra.poly]
    scale_polyDr [prf, in mathcomp.algebra.poly]
    scale_polyE [prf, in mathcomp.algebra.poly]
    scale_row_mx [prf, in mathcomp.algebra.matrix]
    scale_scalar_mx [prf, in mathcomp.algebra.matrix]
    scalel_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scalemx1 [prf, in mathcomp.algebra.matrix]
    scalemx_const [prf, in mathcomp.algebra.matrix]
    scalemx_eq0 [prf, in mathcomp.algebra.matrix]
    scalemx_inj [prf, in mathcomp.algebra.matrix]
    scalemx_key [prf, in mathcomp.algebra.matrix]
    scalemx_sub [prf, in mathcomp.algebra.mxalgebra]
    scalemxA [prf, in mathcomp.algebra.matrix]
    scalemxAl [prf, in mathcomp.algebra.matrix]
    scalemxAr [prf, in mathcomp.algebra.matrix]
    scalemxDl [prf, in mathcomp.algebra.matrix]
    scalemxDr [prf, in mathcomp.algebra.matrix]
    scaleo [prf, in mathcomp.analysis.landau]
    scaleolx [prf, in mathcomp.analysis.landau]
    scaleox [prf, in mathcomp.analysis.landau]
    scaler1 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scaler_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scaler_int [prf, in mathcomp.algebra.ssrint]
    scalerMzl [prf, in mathcomp.algebra.ssrint]
    scalerMzr [prf, in mathcomp.algebra.ssrint]
    scalezrE [prf, in mathcomp.algebra.ssrint]
    scalq_def [prf, in mathcomp.algebra.rat]
    scalq_eq0 [prf, in mathcomp.algebra.rat]
    scalqE [prf, in mathcomp.algebra.rat]
    scalrfctE [prf, in mathcomp.classical.functions]
    scanl_bseqP [prf, in mathcomp.boot.tuple]
    scanl_cat [prf, in mathcomp.boot.seq]
    scanl_rcons [prf, in mathcomp.boot.seq]
    scanl_tupleP [prf, in mathcomp.boot.tuple]
    scanlK [prf, in mathcomp.boot.seq]
    schmidt_complete_unitarymx [prf, in mathcomp.algebra.spectral]
    schmidt_sub [prf, in mathcomp.algebra.spectral]
    schmidt_unitarymx [prf, in mathcomp.algebra.spectral]
    Schur [prf, in mathcomp.algebra.spectral]
    SchurZassenhaus_split [prf, in mathcomp.solvable.hall]
    SchurZassenhaus_trans_actsol [prf, in mathcomp.solvable.hall]
    SchurZassenhaus_trans_sol [prf, in mathcomp.solvable.hall]
    SCN_abelian [prf, in mathcomp.solvable.maximal]
    SCN_max [prf, in mathcomp.solvable.maximal]
    SCN_P [prf, in mathcomp.solvable.maximal]
    Sd1_inj [prf, in mathcomp.solvable.burnside_app]
    sd1_inv [prf, in mathcomp.solvable.burnside_app]
    Sd2_inj [prf, in mathcomp.solvable.burnside_app]
    sd2_inv [prf, in mathcomp.solvable.burnside_app]
    sdpair1_morphM [prf, in mathcomp.finite_group.gproduct]
    sdpair2_morphM [prf, in mathcomp.finite_group.gproduct]
    sdpair_act [prf, in mathcomp.finite_group.gproduct]
    sdpair_setact [prf, in mathcomp.finite_group.gproduct]
    sdpairE [prf, in mathcomp.finite_group.gproduct]
    sdprod1g [prf, in mathcomp.finite_group.gproduct]
    sdprod_card [prf, in mathcomp.finite_group.gproduct]
    sdprod_compl [prf, in mathcomp.finite_group.gproduct]
    sdprod_context [prf, in mathcomp.finite_group.gproduct]
    sdprod_Hall [prf, in mathcomp.solvable.pgroup]
    sdprod_Hall_p'coreP [prf, in mathcomp.solvable.pgroup]
    sdprod_Hall_pcoreP [prf, in mathcomp.solvable.pgroup]
    sdprod_inv_proof [prf, in mathcomp.finite_group.gproduct]
    sdprod_isog [prf, in mathcomp.finite_group.gproduct]
    sdprod_isom [prf, in mathcomp.finite_group.gproduct]
    sdprod_modl [prf, in mathcomp.finite_group.gproduct]
    sdprod_modr [prf, in mathcomp.finite_group.gproduct]
    sdprod_mul1g [prf, in mathcomp.finite_group.gproduct]
    sdprod_mul_proof [prf, in mathcomp.finite_group.gproduct]
    sdprod_mulgA [prf, in mathcomp.finite_group.gproduct]
    sdprod_mulVg [prf, in mathcomp.finite_group.gproduct]
    sdprod_normal_complP [prf, in mathcomp.finite_group.gproduct]
    sdprod_normal_p'HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_normal_pHallP [prf, in mathcomp.solvable.pgroup]
    sdprod_p'core_HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_pcore_HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_recl [prf, in mathcomp.finite_group.gproduct]
    sdprod_recr [prf, in mathcomp.finite_group.gproduct]
    sdprod_sdpair [prf, in mathcomp.finite_group.gproduct]
    sdprod_subr [prf, in mathcomp.finite_group.gproduct]
    sdprodE [prf, in mathcomp.finite_group.gproduct]
    sdprodEY [prf, in mathcomp.finite_group.gproduct]
    sdprodg1 [prf, in mathcomp.finite_group.gproduct]
    sdprodJ [prf, in mathcomp.finite_group.gproduct]
    sdprodm_eqf [prf, in mathcomp.finite_group.gproduct]
    sdprodm_norm [prf, in mathcomp.finite_group.gproduct]
    sdprodm_sub [prf, in mathcomp.finite_group.gproduct]
    sdprodmE [prf, in mathcomp.finite_group.gproduct]
    sdprodmEl [prf, in mathcomp.finite_group.gproduct]
    sdprodmEr [prf, in mathcomp.finite_group.gproduct]
    sdprodP [prf, in mathcomp.finite_group.gproduct]
    sdprodW [prf, in mathcomp.finite_group.gproduct]
    sdprodWC [prf, in mathcomp.finite_group.gproduct]
    sdprodWpp [prf, in mathcomp.finite_group.gproduct]
    sdprodWY [prf, in mathcomp.finite_group.gproduct]
    second_derivative_convex [prf, in mathcomp.analysis.realfun]
    second_isog [prf, in mathcomp.finite_group.quotient]
    second_isom [prf, in mathcomp.finite_group.quotient]
    section_repr_isog [prf, in mathcomp.solvable.jordanholder]
    section_reprP [prf, in mathcomp.solvable.jordanholder]
    segment_can_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_ge [prf, in mathcomp.analysis.realfun]
    segment_can_ge_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_le [prf, in mathcomp.analysis.realfun]
    segment_can_le_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_mono [prf, in mathcomp.analysis.realfun]
    segment_compact [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    segment_connected [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    segment_continuous_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_ge [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_le [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_surjective [prf, in mathcomp.analysis.realfun]
    segment_dec_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_inc_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_mono_surj_continuous [prf, in mathcomp.analysis.realfun]
    semi_additive2E [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_additiveE [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_additiveW [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_sigma_additive_elebesgue_measure [prf, in mathcomp.analysis.lebesgue_measure]
    semi_sigma_additive_is_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_sigma_additive_kproduct [prf, in mathcomp.analysis.kernel]
    semi_sigma_additive_nng_induced [prf, in mathcomp.analysis.charge]
    semi_sigma_additiveE [prf, in mathcomp.analysis.measure_theory.measure_function]
    semidihedral_classP [prf, in mathcomp.solvable.extremal]
    semidihedral_structure [prf, in mathcomp.solvable.extremal]
    SemiGroup.Theory.mulmA [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmAC [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmACA [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmC [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmCA [prf, in mathcomp.boot.bigop]
    semiprime_regular [prf, in mathcomp.solvable.frobenius]
    semiprimeJ [prf, in mathcomp.solvable.frobenius]
    semiprimeS [prf, in mathcomp.solvable.frobenius]
    semiregular1l [prf, in mathcomp.solvable.frobenius]
    semiregular1r [prf, in mathcomp.solvable.frobenius]
    semiregular_prime [prf, in mathcomp.solvable.frobenius]
    semiregular_sym [prf, in mathcomp.solvable.frobenius]
    semiregularJ [prf, in mathcomp.solvable.frobenius]
    semiregularS [prf, in mathcomp.solvable.frobenius]
    semiring_sigma_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    separable_add [prf, in mathcomp.field.separable]
    separable_coprime [prf, in mathcomp.field.separable]
    separable_deriv_eq0 [prf, in mathcomp.field.separable]
    separable_elementP [prf, in mathcomp.field.separable]
    separable_elementS [prf, in mathcomp.field.separable]
    separable_exponent_pchar [prf, in mathcomp.field.separable]
    separable_Fadjoin_seq [prf, in mathcomp.field.separable]
    separable_generator_maximal [prf, in mathcomp.field.separable]
    separable_generator_mem [prf, in mathcomp.field.separable]
    separable_generatorP [prf, in mathcomp.field.separable]
    separable_inseparable_decomposition [prf, in mathcomp.field.separable]
    separable_inseparable_element [prf, in mathcomp.field.separable]
    separable_map [prf, in mathcomp.field.separable]
    separable_mul [prf, in mathcomp.field.separable]
    separable_nosquare [prf, in mathcomp.field.separable]
    separable_nz_der [prf, in mathcomp.field.separable]
    separable_poly_neq0 [prf, in mathcomp.field.separable]
    separable_polyP [prf, in mathcomp.field.separable]
    separable_prod_XsubC [prf, in mathcomp.field.separable]
    separable_refl [prf, in mathcomp.field.separable]
    separable_root [prf, in mathcomp.field.separable]
    separable_root_der [prf, in mathcomp.field.separable]
    separable_sum [prf, in mathcomp.field.separable]
    separable_trans [prf, in mathcomp.field.separable]
    separable_Xn_sub_1 [prf, in mathcomp.field.cyclotomic]
    separableP [prf, in mathcomp.field.separable]
    separablePn_pchar [prf, in mathcomp.field.separable]
    separableS [prf, in mathcomp.field.separable]
    separableSl [prf, in mathcomp.field.separable]
    separableSr [prf, in mathcomp.field.separable]
    separated_closed_ball_countable [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    separated_disjoint [prf, in mathcomp.analysis.topology_theory.connected]
    separated_open_countable [prf, in mathcomp.analysis.topology_theory.num_topology]
    separatedC [prf, in mathcomp.analysis.topology_theory.connected]
    seq1_basis [prf, in mathcomp.algebra.vector]
    seq1_free [prf, in mathcomp.algebra.vector]
    seq_fset_perm [prf, in mathcomp.finmap.finmap]
    seq_fset_uniq [prf, in mathcomp.finmap.finmap]
    seq_fsetE [prf, in mathcomp.finmap.finmap]
    seq_hasChoice [prf, in mathcomp.boot.choice]
    seq_ind2 [prf, in mathcomp.boot.seq]
    seq_mset_id [prf, in mathcomp.finmap.multiset]
    seq_mset_key [prf, in mathcomp.finmap.multiset]
    seq_of_optK [prf, in mathcomp.boot.choice]
    seq_psume_eq0 [prf, in mathcomp.reals.constructive_ereal]
    seq_sub_axiom [prf, in mathcomp.boot.fintype]
    seq_sub_default [prf, in mathcomp.boot.fintype]
    seq_sub_pickleK [prf, in mathcomp.boot.fintype]
    seq_subE [prf, in mathcomp.boot.fintype]
    seq_tnthP [prf, in mathcomp.boot.tuple]
    seqDU_bigcup_eq [prf, in mathcomp.analysis.sequences]
    seqDU_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    seqDU_seqD [prf, in mathcomp.analysis.sequences]
    seqDUE [prf, in mathcomp.analysis.sequences]
    seqDUIE [prf, in mathcomp.analysis.sequences]
    seqs1 [prf, in mathcomp.solvable.burnside_app]
    seqv_sub_adjoin [prf, in mathcomp.field.falgebra]
    series_addn [prf, in mathcomp.analysis.sequences]
    series_cos_coeff0 [prf, in mathcomp.analysis.trigo]
    series_exp_coeff0 [prf, in mathcomp.analysis.sequences]
    series_le_cvg [prf, in mathcomp.analysis.sequences]
    series_sin_coeff0 [prf, in mathcomp.analysis.trigo]
    series_sol [prf, in mathcomp.solvable.nilpotent]
    seriesD [prf, in mathcomp.analysis.sequences]
    seriesEnat [prf, in mathcomp.analysis.sequences]
    seriesEord [prf, in mathcomp.analysis.sequences]
    seriesK [prf, in mathcomp.analysis.sequences]
    seriesN [prf, in mathcomp.analysis.sequences]
    seriesS [prf, in mathcomp.analysis.sequences]
    seriesSB [prf, in mathcomp.analysis.sequences]
    seriesSr [prf, in mathcomp.analysis.sequences]
    seriesZ [prf, in mathcomp.analysis.sequences]
    sesqui_key [prf, in mathcomp.algebra.sesquilinear]
    sesquiE [prf, in mathcomp.algebra.sesquilinear]
    sesquiP [prf, in mathcomp.algebra.sesquilinear]
    set0_Nexists [prf, in mathcomp.boot.finset]
    set0D [prf, in mathcomp.classical.classical_sets]
    set0D [prf, in mathcomp.boot.finset]
    set0fun [prf, in mathcomp.classical.classical_sets]
    set0fun_inj [prf, in mathcomp.classical.functions]
    set0I [prf, in mathcomp.classical.classical_sets]
    set0I [prf, in mathcomp.boot.finset]
    set0P [prf, in mathcomp.classical.classical_sets]
    set0Pn [prf, in mathcomp.boot.finset]
    set0U [prf, in mathcomp.classical.classical_sets]
    set0U [prf, in mathcomp.boot.finset]
    set0X [prf, in mathcomp.classical.classical_sets]
    set0Y [prf, in mathcomp.classical.classical_sets]
    set11 [prf, in mathcomp.boot.finset]
    set1_bigcap_oc [prf, in mathcomp.reals.real_interval]
    set1_inj [prf, in mathcomp.boot.finset]
    set1gE [prf, in mathcomp.finite_group.fingroup]
    set1gP [prf, in mathcomp.finite_group.fingroup]
    set1gXn_commute [prf, in mathcomp.finite_group.gproduct]
    set1gXn_group_set [prf, in mathcomp.finite_group.gproduct]
    set1gXn_key [prf, in mathcomp.finite_group.gproduct]
    set1gXnE [prf, in mathcomp.finite_group.gproduct]
    set1gXnP [prf, in mathcomp.finite_group.gproduct]
    set1I [prf, in mathcomp.classical.classical_sets]
    set1K [prf, in mathcomp.boot.finset]
    set1P [prf, in mathcomp.boot.finset]
    set1Ul [prf, in mathcomp.boot.finset]
    set1Ur [prf, in mathcomp.boot.finset]
    set21 [prf, in mathcomp.boot.finset]
    set22 [prf, in mathcomp.boot.finset]
    set2P [prf, in mathcomp.boot.finset]
    set_0Vmem [prf, in mathcomp.boot.finset]
    set_andb [prf, in mathcomp.classical.classical_sets]
    set_bij00 [prf, in mathcomp.classical.functions]
    set_bij_comp [prf, in mathcomp.classical.functions]
    set_bij_homo [prf, in mathcomp.classical.functions]
    set_bij_inj [prf, in mathcomp.classical.functions]
    set_bij_sub [prf, in mathcomp.classical.functions]
    set_bij_surj [prf, in mathcomp.classical.functions]
    set_bool [prf, in mathcomp.classical.classical_sets]
    set_compose_diag [prf, in mathcomp.classical.classical_sets]
    set_compose_subset [prf, in mathcomp.classical.classical_sets]
    set_cons [prf, in mathcomp.boot.finset]
    set_cons1 [prf, in mathcomp.classical.classical_sets]
    set_cst [prf, in mathcomp.classical.classical_sets]
    set_display [prf, in mathcomp.classical.classical_sets]
    set_enum [prf, in mathcomp.boot.finset]
    set_eq_le [prf, in mathcomp.classical.classical_sets]
    set_false [prf, in mathcomp.classical.classical_sets]
    set_Frobenius_compl [prf, in mathcomp.solvable.frobenius]
    set_fset0 [prf, in mathcomp.classical.classical_sets]
    set_fset1 [prf, in mathcomp.classical.classical_sets]
    set_fset_eq0 [prf, in mathcomp.classical.classical_sets]
    set_fsetD [prf, in mathcomp.classical.classical_sets]
    set_fsetD1 [prf, in mathcomp.classical.classical_sets]
    set_fsetI [prf, in mathcomp.classical.classical_sets]
    set_fsetIr [prf, in mathcomp.classical.classical_sets]
    set_fsetK [prf, in mathcomp.classical.cardinality]
    set_fsetU [prf, in mathcomp.classical.classical_sets]
    set_fsetU1 [prf, in mathcomp.classical.classical_sets]
    set_fun_image [prf, in mathcomp.classical.functions]
    set_imfset [prf, in mathcomp.classical.classical_sets]
    set_invgK [prf, in mathcomp.finite_group.fingroup]
    set_invgM [prf, in mathcomp.finite_group.fingroup]
    set_iterF_mono [prf, in mathcomp.finmap.finmap]
    set_iterF_sub [prf, in mathcomp.finmap.finmap]
    set_itv1 [prf, in mathcomp.classical.set_interval]
    set_itv_bndNy [prf, in mathcomp.classical.set_interval]
    set_itv_ge [prf, in mathcomp.classical.set_interval]
    set_itv_setT [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    set_itv_splitD [prf, in mathcomp.classical.set_interval]
    set_itv_splitI [prf, in mathcomp.classical.set_interval]
    set_itv_splitU [prf, in mathcomp.classical.set_interval]
    set_itv_ybnd [prf, in mathcomp.classical.set_interval]
    set_itvcc [prf, in mathcomp.classical.set_interval]
    set_itvco [prf, in mathcomp.classical.set_interval]
    set_itvco0 [prf, in mathcomp.classical.set_interval]
    set_itvcy [prf, in mathcomp.classical.set_interval]
    set_itvI [prf, in mathcomp.classical.set_interval]
    set_itvK [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    set_itvNyc [prf, in mathcomp.classical.set_interval]
    set_itvNyo [prf, in mathcomp.classical.set_interval]
    set_itvNyy [prf, in mathcomp.classical.set_interval]
    set_itvoc [prf, in mathcomp.classical.set_interval]
    set_itvoc0 [prf, in mathcomp.classical.set_interval]
    set_itvoo [prf, in mathcomp.classical.set_interval]
    set_itvoo0 [prf, in mathcomp.classical.set_interval]
    set_itvoy [prf, in mathcomp.classical.set_interval]
    set_itvP [prf, in mathcomp.classical.set_interval]
    set_itvxx [prf, in mathcomp.classical.set_interval]
    set_last_default [prf, in mathcomp.boot.seq]
    set_lte_bigcup [prf, in mathcomp.reals.real_interval]
    set_mem [prf, in mathcomp.classical.classical_sets]
    set_mem_set [prf, in mathcomp.classical.classical_sets]
    set_memK [prf, in mathcomp.classical.classical_sets]
    set_mul1g [prf, in mathcomp.finite_group.fingroup]
    set_mulgA [prf, in mathcomp.finite_group.fingroup]
    set_nbhsP [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    set_neq_lt [prf, in mathcomp.classical.classical_sets]
    set_nil [prf, in mathcomp.classical.classical_sets]
    set_nil [prf, in mathcomp.boot.finset]
    set_nth_default [prf, in mathcomp.boot.seq]
    set_nth_nil [prf, in mathcomp.boot.seq]
    set_nthE [prf, in mathcomp.boot.seq]
    set_orb [prf, in mathcomp.classical.classical_sets]
    set_partition_big [prf, in mathcomp.boot.finset]
    set_partition_big_cond [prf, in mathcomp.boot.finset]
    set_predC [prf, in mathcomp.classical.classical_sets]
    set_prod_invK [prf, in mathcomp.classical.classical_sets]
    set_seq1 [prf, in mathcomp.boot.finset]
    set_seq_eq0 [prf, in mathcomp.classical.classical_sets]
    set_set_nth [prf, in mathcomp.boot.seq]
    set_true [prf, in mathcomp.classical.classical_sets]
    set_unit [prf, in mathcomp.classical.classical_sets]
    set_valE [prf, in mathcomp.classical.functions]
    set_valP [prf, in mathcomp.classical.classical_sets]
    setact_is_action [prf, in mathcomp.finite_group.action]
    setact_orbit [prf, in mathcomp.finite_group.action]
    setactE [prf, in mathcomp.finite_group.action]
    setactJ [prf, in mathcomp.finite_group.action]
    setactVin [prf, in mathcomp.finite_group.action]
    setC0 [prf, in mathcomp.classical.classical_sets]
    setC0 [prf, in mathcomp.boot.finset]
    setC11 [prf, in mathcomp.boot.finset]
    setC_bigcap [prf, in mathcomp.classical.classical_sets]
    setC_bigcap [prf, in mathcomp.boot.finset]
    setC_bigcup [prf, in mathcomp.classical.classical_sets]
    setC_bigcup [prf, in mathcomp.boot.finset]
    setC_bigsetI [prf, in mathcomp.classical.classical_sets]
    setC_bigsetU [prf, in mathcomp.classical.classical_sets]
    setC_I [prf, in mathcomp.classical.classical_sets]
    setC_inj [prf, in mathcomp.boot.finset]
    setCD [prf, in mathcomp.classical.classical_sets]
    setCD [prf, in mathcomp.boot.finset]
    setCI [prf, in mathcomp.classical.classical_sets]
    setCI [prf, in mathcomp.boot.finset]
    setCitv [prf, in mathcomp.classical.set_interval]
    setCitvl [prf, in mathcomp.classical.set_interval]
    setCitvr [prf, in mathcomp.classical.set_interval]
    setCK [prf, in mathcomp.classical.classical_sets]
    setCK [prf, in mathcomp.boot.finset]
    setCP [prf, in mathcomp.boot.finset]
    setCS [prf, in mathcomp.classical.classical_sets]
    setCS [prf, in mathcomp.boot.finset]
    setCT [prf, in mathcomp.classical.classical_sets]
    setCT [prf, in mathcomp.boot.finset]
    setCU [prf, in mathcomp.classical.classical_sets]
    setCU [prf, in mathcomp.boot.finset]
    setCU_Efin [prf, in mathcomp.analysis.measurable_realfun]
    setCYT [prf, in mathcomp.classical.classical_sets]
    setD0 [prf, in mathcomp.classical.classical_sets]
    setD0 [prf, in mathcomp.boot.finset]
    setD11 [prf, in mathcomp.boot.finset]
    setD1K [prf, in mathcomp.classical.classical_sets]
    setD1K [prf, in mathcomp.boot.finset]
    setD1P [prf, in mathcomp.boot.finset]
    setD_bigcup [prf, in mathcomp.classical.classical_sets]
    setD_bigcupl [prf, in mathcomp.classical.classical_sets]
    setD_bndc_Nybnd [prf, in mathcomp.classical.set_interval]
    setD_cbnd_bndy [prf, in mathcomp.classical.set_interval]
    setD_closedP [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setD_eq0 [prf, in mathcomp.finmap.multiset]
    setD_eq0 [prf, in mathcomp.classical.classical_sets]
    setD_eq0 [prf, in mathcomp.boot.finset]
    setD_semi_setD_closed [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setDccitv [prf, in mathcomp.classical.set_interval]
    setDD [prf, in mathcomp.classical.classical_sets]
    setDDl [prf, in mathcomp.classical.classical_sets]
    setDDl [prf, in mathcomp.boot.finset]
    setDDr [prf, in mathcomp.classical.classical_sets]
    setDDr [prf, in mathcomp.boot.finset]
    setDE [prf, in mathcomp.classical.classical_sets]
    setDE [prf, in mathcomp.boot.finset]
    setDidl [prf, in mathcomp.classical.classical_sets]
    setDidPl [prf, in mathcomp.classical.classical_sets]
    setDidPl [prf, in mathcomp.boot.finset]
    setDIK [prf, in mathcomp.classical.classical_sets]
    setDIl [prf, in mathcomp.boot.finset]
    setDIr [prf, in mathcomp.classical.classical_sets]
    setDIr [prf, in mathcomp.boot.finset]
    setDitv1l [prf, in mathcomp.classical.set_interval]
    setDitv1r [prf, in mathcomp.classical.set_interval]
    setDitv_set2 [prf, in mathcomp.classical.set_interval]
    setDitvNyo [prf, in mathcomp.classical.set_interval]
    setDitvoo [prf, in mathcomp.classical.set_interval]
    setDitvoy [prf, in mathcomp.classical.set_interval]
    setDKI [prf, in mathcomp.classical.classical_sets]
    setDKU [prf, in mathcomp.classical.classical_sets]
    setDP [prf, in mathcomp.boot.finset]
    setDS [prf, in mathcomp.classical.classical_sets]
    setDS [prf, in mathcomp.boot.finset]
    setDSS [prf, in mathcomp.classical.classical_sets]
    setDSS [prf, in mathcomp.boot.finset]
    setDT [prf, in mathcomp.classical.classical_sets]
    setDT [prf, in mathcomp.boot.finset]
    setDU [prf, in mathcomp.classical.classical_sets]
    setDUD [prf, in mathcomp.classical.classical_sets]
    setDUK [prf, in mathcomp.classical.classical_sets]
    setDUl [prf, in mathcomp.classical.classical_sets]
    setDUl [prf, in mathcomp.boot.finset]
    setDUr [prf, in mathcomp.classical.classical_sets]
    setDUr [prf, in mathcomp.boot.finset]
    setDv [prf, in mathcomp.classical.classical_sets]
    setDv [prf, in mathcomp.boot.finset]
    seteqP [prf, in mathcomp.classical.classical_sets]
    setf_catl [prf, in mathcomp.finmap.finmap]
    setf_catr [prf, in mathcomp.finmap.finmap]
    setF_eq0 [prf, in mathcomp.classical.classical_sets]
    setf_get [prf, in mathcomp.finmap.finmap]
    setf_inj [prf, in mathcomp.finmap.finmap]
    setf_rem [prf, in mathcomp.finmap.finmap]
    setf_rem1 [prf, in mathcomp.finmap.finmap]
    setf_restrict [prf, in mathcomp.finmap.finmap]
    setfC [prf, in mathcomp.finmap.finmap]
    setfK [prf, in mathcomp.finmap.finmap]
    setfNK [prf, in mathcomp.finmap.finmap]
    setI0 [prf, in mathcomp.classical.classical_sets]
    setI0 [prf, in mathcomp.boot.finset]
    setI1 [prf, in mathcomp.classical.classical_sets]
    setI1g [prf, in mathcomp.finite_group.fingroup]
    setI_bigcupl [prf, in mathcomp.classical.classical_sets]
    setI_bigcupr [prf, in mathcomp.classical.classical_sets]
    setI_closed_g_dynkin_g_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setI_eq0 [prf, in mathcomp.boot.finset]
    setI_g_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setI_II [prf, in mathcomp.classical.classical_sets]
    setI_im_cpair [prf, in mathcomp.solvable.center]
    setI_normal_Hall [prf, in mathcomp.solvable.pgroup]
    setI_powerset [prf, in mathcomp.boot.finset]
    setI_subnormal [prf, in mathcomp.solvable.gseries]
    setI_transversal_pblock [prf, in mathcomp.boot.finset]
    setIA [prf, in mathcomp.classical.classical_sets]
    setIA [prf, in mathcomp.boot.finset]
    setIAC [prf, in mathcomp.classical.classical_sets]
    setIAC [prf, in mathcomp.boot.finset]
    setIACA [prf, in mathcomp.classical.classical_sets]
    setIACA [prf, in mathcomp.boot.finset]
    setIC [prf, in mathcomp.classical.classical_sets]
    setIC [prf, in mathcomp.boot.finset]
    setICA [prf, in mathcomp.classical.classical_sets]
    setICA [prf, in mathcomp.boot.finset]
    setICK [prf, in mathcomp.classical.classical_sets]
    setICl [prf, in mathcomp.classical.classical_sets]
    setICr [prf, in mathcomp.classical.classical_sets]
    setICr [prf, in mathcomp.boot.finset]
    setID [prf, in mathcomp.boot.finset]
    setId2P [prf, in mathcomp.boot.finset]
    setIDA [prf, in mathcomp.classical.classical_sets]
    setIDA [prf, in mathcomp.boot.finset]
    setIDAC [prf, in mathcomp.classical.classical_sets]
    setIDAC [prf, in mathcomp.boot.finset]
    setIdE [prf, in mathcomp.boot.finset]
    setIdP [prf, in mathcomp.boot.finset]
    setIg1 [prf, in mathcomp.finite_group.fingroup]
    setIid [prf, in mathcomp.classical.classical_sets]
    setIid [prf, in mathcomp.boot.finset]
    setIidl [prf, in mathcomp.classical.classical_sets]
    setIidPl [prf, in mathcomp.classical.classical_sets]
    setIidPl [prf, in mathcomp.boot.finset]
    setIidPr [prf, in mathcomp.classical.classical_sets]
    setIidPr [prf, in mathcomp.boot.finset]
    setIidr [prf, in mathcomp.classical.classical_sets]
    setIIl [prf, in mathcomp.classical.classical_sets]
    setIIl [prf, in mathcomp.boot.finset]
    setIIr [prf, in mathcomp.classical.classical_sets]
    setIIr [prf, in mathcomp.boot.finset]
    setIK [prf, in mathcomp.classical.classical_sets]
    setIK [prf, in mathcomp.boot.finset]
    setIKC [prf, in mathcomp.classical.classical_sets]
    setIP [prf, in mathcomp.boot.finset]
    setIS [prf, in mathcomp.classical.classical_sets]
    setIS [prf, in mathcomp.boot.finset]
    setISS [prf, in mathcomp.classical.classical_sets]
    setISS [prf, in mathcomp.boot.finset]
    setIT [prf, in mathcomp.classical.classical_sets]
    setIT [prf, in mathcomp.boot.finset]
    setitv0 [prf, in mathcomp.classical.set_interval]
    setIUl [prf, in mathcomp.classical.classical_sets]
    setIUl [prf, in mathcomp.boot.finset]
    setIUr [prf, in mathcomp.classical.classical_sets]
    setIUr [prf, in mathcomp.boot.finset]
    setIYl [prf, in mathcomp.classical.classical_sets]
    setIYr [prf, in mathcomp.classical.classical_sets]
    setKI [prf, in mathcomp.classical.classical_sets]
    setKI [prf, in mathcomp.boot.finset]
    setKU [prf, in mathcomp.classical.classical_sets]
    setKU [prf, in mathcomp.boot.finset]
    setNK [prf, in mathcomp.classical.set_interval]
    SetOrder.Exports.botEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.complEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.joinEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.meetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.topEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinIB [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinKI [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.le_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.lt_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.meetKU [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_setTsub [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_sub0set [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.subKI [prf, in mathcomp.classical.classical_sets]
    setP [prf, in mathcomp.boot.finset]
    SetRing.all_decomp_neq0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.cover_decomp [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_finite_set [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_measurable [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_neq0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_set0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_sub [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_triv [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decompN0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.measurable_subring [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.ring_finite_set [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.ring_measurableE [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_fin_bigcup [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_ge0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.RmuE [prf, in mathcomp.analysis.measure_theory.measure_function]
    setring0 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_fin_bigcup [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_id [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_monotone_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setringD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setringU [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setSD [prf, in mathcomp.classical.classical_sets]
    setSD [prf, in mathcomp.boot.finset]
    setSI [prf, in mathcomp.classical.classical_sets]
    setSI [prf, in mathcomp.boot.finset]
    setSU [prf, in mathcomp.classical.classical_sets]
    setSU [prf, in mathcomp.boot.finset]
    setSX [prf, in mathcomp.classical.classical_sets]
    setT0 [prf, in mathcomp.classical.classical_sets]
    setT_bool [prf, in mathcomp.classical.classical_sets]
    setT_unit [prf, in mathcomp.classical.classical_sets]
    setTD [prf, in mathcomp.classical.classical_sets]
    setTD [prf, in mathcomp.boot.finset]
    setTI [prf, in mathcomp.classical.classical_sets]
    setTI [prf, in mathcomp.boot.finset]
    setTPn [prf, in mathcomp.classical.classical_sets]
    setTT_bijective [prf, in mathcomp.classical.functions]
    setTU [prf, in mathcomp.classical.classical_sets]
    setTU [prf, in mathcomp.boot.finset]
    setTX [prf, in mathcomp.classical.classical_sets]
    setTYC [prf, in mathcomp.classical.classical_sets]
    setU0 [prf, in mathcomp.classical.classical_sets]
    setU0 [prf, in mathcomp.boot.finset]
    setU11 [prf, in mathcomp.boot.finset]
    setU1itv [prf, in mathcomp.classical.set_interval]
    setU1K [prf, in mathcomp.boot.finset]
    setU1P [prf, in mathcomp.boot.finset]
    setU1r [prf, in mathcomp.boot.finset]
    setU_bigcapl [prf, in mathcomp.classical.classical_sets]
    setU_bigcapr [prf, in mathcomp.classical.classical_sets]
    setU_eq0 [prf, in mathcomp.classical.classical_sets]
    setU_eq0 [prf, in mathcomp.boot.finset]
    setU_id2r [prf, in mathcomp.classical.classical_sets]
    setU_II [prf, in mathcomp.classical.classical_sets]
    setU_seqD [prf, in mathcomp.analysis.sequences]
    setUA [prf, in mathcomp.classical.classical_sets]
    setUA [prf, in mathcomp.boot.finset]
    setUAC [prf, in mathcomp.classical.classical_sets]
    setUAC [prf, in mathcomp.boot.finset]
    setUACA [prf, in mathcomp.classical.classical_sets]
    setUACA [prf, in mathcomp.boot.finset]
    setUC [prf, in mathcomp.classical.classical_sets]
    setUC [prf, in mathcomp.boot.finset]
    setUCA [prf, in mathcomp.classical.classical_sets]
    setUCA [prf, in mathcomp.boot.finset]
    setUCK [prf, in mathcomp.classical.classical_sets]
    setUCl [prf, in mathcomp.classical.classical_sets]
    setUCr [prf, in mathcomp.classical.classical_sets]
    setUCr [prf, in mathcomp.boot.finset]
    setUD [prf, in mathcomp.boot.finset]
    setUDK [prf, in mathcomp.classical.classical_sets]
    setUDl [prf, in mathcomp.classical.classical_sets]
    setUDl [prf, in mathcomp.boot.finset]
    setUDr [prf, in mathcomp.classical.classical_sets]
    setUid [prf, in mathcomp.classical.classical_sets]
    setUid [prf, in mathcomp.boot.finset]
    setUIDK [prf, in mathcomp.classical.classical_sets]
    setUidl [prf, in mathcomp.classical.classical_sets]
    setUidPl [prf, in mathcomp.classical.classical_sets]
    setUidPl [prf, in mathcomp.boot.finset]
    setUidPr [prf, in mathcomp.classical.classical_sets]
    setUidPr [prf, in mathcomp.boot.finset]
    setUidr [prf, in mathcomp.classical.classical_sets]
    setUIl [prf, in mathcomp.classical.classical_sets]
    setUIl [prf, in mathcomp.boot.finset]
    setUIr [prf, in mathcomp.classical.classical_sets]
    setUIr [prf, in mathcomp.boot.finset]
    setUitv1 [prf, in mathcomp.classical.set_interval]
    setUitv_set2 [prf, in mathcomp.classical.set_interval]
    setUK [prf, in mathcomp.classical.classical_sets]
    setUK [prf, in mathcomp.boot.finset]
    setUKC [prf, in mathcomp.classical.classical_sets]
    setUKD [prf, in mathcomp.classical.classical_sets]
    setUP [prf, in mathcomp.boot.finset]
    setUS [prf, in mathcomp.classical.classical_sets]
    setUS [prf, in mathcomp.boot.finset]
    setUSS [prf, in mathcomp.classical.classical_sets]
    setUSS [prf, in mathcomp.boot.finset]
    setUT [prf, in mathcomp.classical.classical_sets]
    setUT [prf, in mathcomp.boot.finset]
    setUUl [prf, in mathcomp.classical.classical_sets]
    setUUl [prf, in mathcomp.boot.finset]
    setUUr [prf, in mathcomp.classical.classical_sets]
    setUUr [prf, in mathcomp.boot.finset]
    setUv [prf, in mathcomp.classical.classical_sets]
    setvU [prf, in mathcomp.classical.classical_sets]
    setX0 [prf, in mathcomp.classical.classical_sets]
    setX_bigcupl [prf, in mathcomp.classical.classical_sets]
    setX_bigcupr [prf, in mathcomp.classical.classical_sets]
    setX_dprod [prf, in mathcomp.finite_group.gproduct]
    setX_gen [prf, in mathcomp.finite_group.gproduct]
    setX_of_sigT_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_of_sigTK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_prod [prf, in mathcomp.finite_group.gproduct]
    setXI [prf, in mathcomp.classical.classical_sets]
    setXn_dprod [prf, in mathcomp.finite_group.gproduct]
    setXn_gen [prf, in mathcomp.finite_group.gproduct]
    setXn_prod [prf, in mathcomp.finite_group.gproduct]
    setXn_sol [prf, in mathcomp.solvable.nilpotent]
    setXnP [prf, in mathcomp.boot.finset]
    setXnS [prf, in mathcomp.boot.finset]
    setXP [prf, in mathcomp.boot.finset]
    setXS [prf, in mathcomp.boot.finset]
    setXT [prf, in mathcomp.classical.classical_sets]
    setXTT [prf, in mathcomp.classical.classical_sets]
    setY0 [prf, in mathcomp.classical.classical_sets]
    setY_def [prf, in mathcomp.classical.classical_sets]
    setYA [prf, in mathcomp.classical.classical_sets]
    setYC [prf, in mathcomp.classical.classical_sets]
    setYCT [prf, in mathcomp.classical.classical_sets]
    setYD [prf, in mathcomp.classical.classical_sets]
    setYE [prf, in mathcomp.classical.classical_sets]
    setYI [prf, in mathcomp.classical.classical_sets]
    setYK [prf, in mathcomp.classical.classical_sets]
    setYTC [prf, in mathcomp.classical.classical_sets]
    setYU [prf, in mathcomp.classical.classical_sets]
    sfinite_Fubini [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfinite_kernel [prf, in mathcomp.analysis.kernel]
    sfinite_kernel_measure [prf, in mathcomp.analysis.kernel]
    sfinite_measure_seqP [prf, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_measure_sigma_finite [prf, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_mzero [prf, in mathcomp.analysis.measure_theory.measure_function]
    sfun0 [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun1 [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_fubini_tonelli [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli1 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli2 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli_FE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli_GE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_measurable_fun_fubini_tonelli_F [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_measurable_fun_fubini_tonelli_G [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_prod [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_rect [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_subring_closed [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_sum [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_valP [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunB [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunD [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfuneqP [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunM [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunN [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunX [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sgr_denq [prf, in mathcomp.algebra.rat]
    sgr_numq [prf, in mathcomp.algebra.rat]
    sgr_numq_div [prf, in mathcomp.algebra.rat]
    sgr_scalq [prf, in mathcomp.algebra.rat]
    sgrEz [prf, in mathcomp.algebra.ssrint]
    sgrMz [prf, in mathcomp.algebra.ssrint]
    sgrz [prf, in mathcomp.algebra.ssrint]
    sgval_sub [prf, in mathcomp.finite_group.morphism]
    sgvalK [prf, in mathcomp.finite_group.fingroup]
    sgvalM [prf, in mathcomp.finite_group.fingroup]
    sgvalmK [prf, in mathcomp.finite_group.morphism]
    sgz0 [prf, in mathcomp.algebra.ssrint]
    sgz1 [prf, in mathcomp.algebra.ssrint]
    sgz_contents [prf, in mathcomp.algebra.intdiv]
    sgz_cp0 [prf, in mathcomp.algebra.ssrint]
    sgz_def [prf, in mathcomp.algebra.ssrint]
    sgz_eq [prf, in mathcomp.algebra.ssrint]
    sgz_eq0 [prf, in mathcomp.algebra.ssrint]
    sgz_ge0 [prf, in mathcomp.algebra.ssrint]
    sgz_gt0 [prf, in mathcomp.algebra.ssrint]
    sgz_id [prf, in mathcomp.algebra.ssrint]
    sgz_int [prf, in mathcomp.algebra.ssrint]
    sgz_le0 [prf, in mathcomp.algebra.ssrint]
    sgz_lead_primitive [prf, in mathcomp.algebra.intdiv]
    sgz_lt0 [prf, in mathcomp.algebra.ssrint]
    sgz_odd [prf, in mathcomp.algebra.ssrint]
    sgz_sgr [prf, in mathcomp.algebra.ssrint]
    sgz_smul [prf, in mathcomp.algebra.ssrint]
    sgzM [prf, in mathcomp.algebra.ssrint]
    sgzN [prf, in mathcomp.algebra.ssrint]
    sgzN1 [prf, in mathcomp.algebra.ssrint]
    sgzP [prf, in mathcomp.algebra.ssrint]
    sgzX [prf, in mathcomp.algebra.ssrint]
    Sh_inj [prf, in mathcomp.solvable.burnside_app]
    sh_inv [prf, in mathcomp.solvable.burnside_app]
    shape_rev [prf, in mathcomp.boot.seq]
    shift0 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    shortenP [prf, in mathcomp.boot.path]
    showo [prf, in mathcomp.analysis.landau]
    sig2_eqW [prf, in mathcomp.boot.choice]
    sig2W [prf, in mathcomp.boot.choice]
    sig_big_dep [prf, in mathcomp.boot.bigop]
    sig_big_dep_idem [prf, in mathcomp.boot.bigop]
    sig_eq2W [prf, in mathcomp.boot.choice]
    sig_eqW [prf, in mathcomp.boot.choice]
    sigL2K [prf, in mathcomp.classical.functions]
    sigL_bijP [prf, in mathcomp.classical.functions]
    sigL_funP [prf, in mathcomp.classical.functions]
    sigL_injP [prf, in mathcomp.classical.functions]
    sigL_isfun [prf, in mathcomp.classical.functions]
    sigL_restrict [prf, in mathcomp.classical.functions]
    sigL_some_inv [prf, in mathcomp.classical.functions]
    sigL_surjP [prf, in mathcomp.classical.functions]
    sigL_valL [prf, in mathcomp.classical.functions]
    sigL_valLfun [prf, in mathcomp.classical.functions]
    sigLE [prf, in mathcomp.classical.functions]
    sigLK [prf, in mathcomp.classical.functions]
    sigLR_bijP [prf, in mathcomp.classical.functions]
    sigLR_injP [prf, in mathcomp.classical.functions]
    sigLR_surjP [prf, in mathcomp.classical.functions]
    sigLRfun_bijP [prf, in mathcomp.classical.functions]
    sigma_additive_is_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_algebra0 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_bigcap [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_bigcup [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_dynkin [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_id [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_image [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_preimage [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_strace [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraCD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraP [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_finite_counting [prf, in mathcomp.analysis.measure_theory.counting_measure]
    sigma_finite_mkproduct [prf, in mathcomp.analysis.kernel]
    sigma_finite_mzero [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_finiteP [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_ring_monotone [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigmaRingType_lambda_system [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    signed_intro [prf, in mathcomp.reals.signed]
    signed_le_total [prf, in mathcomp.reals.signed]
    signr_scalq [prf, in mathcomp.algebra.rat]
    sigR_funK [prf, in mathcomp.classical.functions]
    sigR_some_inv [prf, in mathcomp.classical.functions]
    sigRK [prf, in mathcomp.classical.functions]
    sigT_compact [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_continuous [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    sigT_nbhs_nbhs [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_proper [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_singleton [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhsE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_of_setX_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_of_setXK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_openP [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_setUE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigW [prf, in mathcomp.boot.choice]
    similar_diag_mxminpoly [prf, in mathcomp.algebra.mxred]
    similar_diag_row_base [prf, in mathcomp.algebra.mxred]
    similar_diag_sum [prf, in mathcomp.algebra.mxred]
    similar_diagLR [prf, in mathcomp.algebra.mxred]
    similar_diagP [prf, in mathcomp.algebra.mxred]
    similar_diagPex [prf, in mathcomp.algebra.mxred]
    similar_diagPp [prf, in mathcomp.algebra.mxred]
    similar_mxminpoly [prf, in mathcomp.algebra.mxred]
    similarLR [prf, in mathcomp.algebra.mxred]
    similarP [prf, in mathcomp.algebra.mxred]
    similarPp [prf, in mathcomp.algebra.mxred]
    similarRL [prf, in mathcomp.algebra.mxred]
    similarW [prf, in mathcomp.algebra.mxred]
    simmx_minpoly [prf, in mathcomp.algebra.mxpoly]
    simmxLR [prf, in mathcomp.algebra.mxpoly]
    simmxP [prf, in mathcomp.algebra.mxpoly]
    simmxPp [prf, in mathcomp.algebra.mxpoly]
    simmxRL [prf, in mathcomp.algebra.mxpoly]
    simmxW [prf, in mathcomp.algebra.mxpoly]
    simple_Alt5 [prf, in mathcomp.solvable.alt]
    simple_Alt5_base [prf, in mathcomp.solvable.alt]
    simple_Alt_3 [prf, in mathcomp.solvable.alt]
    simple_bounded [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    simple_compsP [prf, in mathcomp.solvable.jordanholder]
    simple_maxnormal [prf, in mathcomp.solvable.gseries]
    simple_sol_prime [prf, in mathcomp.solvable.maximal]
    simpleP [prf, in mathcomp.solvable.gseries]
    sin0 [prf, in mathcomp.analysis.trigo]
    sin0cos1 [prf, in mathcomp.analysis.trigo]
    sin1cos0 [prf, in mathcomp.analysis.trigo]
    sin2_gt0 [prf, in mathcomp.analysis.trigo]
    sin2cos2 [prf, in mathcomp.analysis.trigo]
    sin2pi [prf, in mathcomp.analysis.trigo]
    sin_acos [prf, in mathcomp.analysis.trigo]
    sin_coeff'E [prf, in mathcomp.analysis.trigo]
    sin_coeff_even [prf, in mathcomp.analysis.trigo]
    sin_coeffE [prf, in mathcomp.analysis.trigo]
    sin_ge0_pi [prf, in mathcomp.analysis.trigo]
    sin_geN1 [prf, in mathcomp.analysis.trigo]
    sin_gt0_pi [prf, in mathcomp.analysis.trigo]
    sin_gt0_pihalf [prf, in mathcomp.analysis.trigo]
    sin_inj [prf, in mathcomp.analysis.trigo]
    sin_le1 [prf, in mathcomp.analysis.trigo]
    sin_max [prf, in mathcomp.analysis.trigo]
    sin_mulr2n [prf, in mathcomp.analysis.trigo]
    sin_pihalf [prf, in mathcomp.analysis.trigo]
    sin_sg [prf, in mathcomp.analysis.trigo]
    sinB [prf, in mathcomp.analysis.trigo]
    sinBpihalf [prf, in mathcomp.analysis.trigo]
    sinD [prf, in mathcomp.analysis.trigo]
    sinD2pi [prf, in mathcomp.analysis.trigo]
    sinD_cosD [prf, in mathcomp.analysis.trigo]
    sinDpi [prf, in mathcomp.analysis.trigo]
    sinDpihalf [prf, in mathcomp.analysis.trigo]
    sinE [prf, in mathcomp.analysis.trigo]
    sinK [prf, in mathcomp.analysis.trigo]
    sinN [prf, in mathcomp.analysis.trigo]
    sinN_cosN [prf, in mathcomp.analysis.trigo]
    sinpi [prf, in mathcomp.analysis.trigo]
    sintegral0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegral_EFin_cst [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
    sintegral_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegral_giry_join [prf, in mathcomp.analysis.lebesgue_integral_theory.giry]
    sintegral_indic [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralD [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralEnnsfun [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralET [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralrM [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    size0nil [prf, in mathcomp.boot.seq]
    size1_polyC [prf, in mathcomp.algebra.poly]
    size1_zip [prf, in mathcomp.boot.seq]
    size2_zip [prf, in mathcomp.boot.seq]
    size_abelian_type [prf, in mathcomp.solvable.abelian]
    size_algC_pfactor [prf, in mathcomp.field.algC]
    size_algR_pfactor [prf, in mathcomp.field.algC]
    size_allpairs [prf, in mathcomp.boot.seq]
    size_allpairs_dep [prf, in mathcomp.boot.seq]
    size_basis [prf, in mathcomp.algebra.vector]
    size_behead [prf, in mathcomp.boot.seq]
    size_belast [prf, in mathcomp.boot.seq]
    size_bseq [prf, in mathcomp.boot.tuple]
    size_cast_bseq [prf, in mathcomp.boot.tuple]
    size_cat [prf, in mathcomp.boot.seq]
    size_char_poly [prf, in mathcomp.algebra.mxpoly]
    size_Cmul [prf, in mathcomp.algebra.poly]
    size_codom [prf, in mathcomp.boot.fintype]
    size_comp_poly [prf, in mathcomp.algebra.poly]
    size_comp_poly2 [prf, in mathcomp.algebra.poly]
    size_comp_poly_leq [prf, in mathcomp.algebra.poly]
    size_cons_poly [prf, in mathcomp.algebra.poly]
    size_Cyclotomic [prf, in mathcomp.field.cyclotomic]
    size_cyclotomic [prf, in mathcomp.field.cyclotomic]
    size_drop [prf, in mathcomp.boot.seq]
    size_drop_poly [prf, in mathcomp.algebra.poly]
    size_enum_ord [prf, in mathcomp.boot.fintype]
    size_eq0 [prf, in mathcomp.boot.seq]
    size_even_poly [prf, in mathcomp.algebra.poly]
    size_even_poly_eq [prf, in mathcomp.algebra.poly]
    size_exp [prf, in mathcomp.algebra.poly]
    size_exp_XsubC [prf, in mathcomp.algebra.poly]
    size_Fadjoin_poly [prf, in mathcomp.field.fieldext]
    size_filter [prf, in mathcomp.boot.seq]
    size_filter_gt0 [prf, in mathcomp.classical.unstable]
    size_filter_gt0 [prf, in mathcomp.boot.seq]
    size_flatten [prf, in mathcomp.boot.seq]
    size_image [prf, in mathcomp.boot.fintype]
    size_incr_nth [prf, in mathcomp.boot.seq]
    size_infix [prf, in mathcomp.boot.seq]
    size_insub_bseq [prf, in mathcomp.boot.tuple]
    size_iota [prf, in mathcomp.boot.seq]
    size_lagrange [prf, in mathcomp.algebra.qpoly]
    size_lagrange_ [prf, in mathcomp.algebra.qpoly]
    size_map [prf, in mathcomp.boot.seq]
    size_map_inj_poly [prf, in mathcomp.algebra.poly]
    size_map_poly [prf, in mathcomp.algebra.poly]
    size_map_poly_id0 [prf, in mathcomp.algebra.poly]
    size_map_polyC [prf, in mathcomp.algebra.poly]
    size_mask [prf, in mathcomp.boot.seq]
    size_merge [prf, in mathcomp.boot.path]
    size_merge_sort_push [prf, in mathcomp.boot.path]
    size_minCpoly [prf, in mathcomp.field.algC]
    size_minPoly [prf, in mathcomp.field.fieldext]
    size_mk_monic [prf, in mathcomp.algebra.qpoly]
    size_mk_monic_gt0 [prf, in mathcomp.algebra.qpoly]
    size_mk_monic_gt1 [prf, in mathcomp.algebra.qpoly]
    size_mkseq [prf, in mathcomp.boot.seq]
    size_Mmonic [prf, in mathcomp.algebra.poly]
    size_mod_mxminpoly [prf, in mathcomp.algebra.mxpoly]
    size_monicM [prf, in mathcomp.algebra.poly]
    size_mset0 [prf, in mathcomp.finmap.multiset]
    size_mset_eq0 [prf, in mathcomp.finmap.multiset]
    size_Msign [prf, in mathcomp.algebra.poly]
    size_mul [prf, in mathcomp.algebra.poly]
    size_mul_eq1 [prf, in mathcomp.algebra.poly]
    size_mulX [prf, in mathcomp.algebra.poly]
    size_mulXn [prf, in mathcomp.algebra.poly]
    size_MXaddC [prf, in mathcomp.algebra.poly]
    size_mxminpoly [prf, in mathcomp.algebra.mxpoly]
    size_ncons [prf, in mathcomp.boot.seq]
    size_npoly [prf, in mathcomp.algebra.qpoly]
    size_npoly0 [prf, in mathcomp.algebra.qpoly]
    size_nseq [prf, in mathcomp.boot.seq]
    size_odd_poly [prf, in mathcomp.algebra.poly]
    size_odd_poly_eq [prf, in mathcomp.algebra.poly]
    size_orbit [prf, in mathcomp.boot.fingraph]
    size_pairmap [prf, in mathcomp.boot.seq]
    size_permutations [prf, in mathcomp.boot.seq]
    size_pmap [prf, in mathcomp.boot.seq]
    size_pmap_sub [prf, in mathcomp.boot.seq]
    size_poly [prf, in mathcomp.algebra.poly]
    size_Poly [prf, in mathcomp.algebra.poly]
    size_poly0 [prf, in mathcomp.algebra.poly]
    size_poly1 [prf, in mathcomp.algebra.poly]
    size_poly1P [prf, in mathcomp.algebra.poly]
    size_poly_eq [prf, in mathcomp.algebra.poly]
    size_poly_eq0 [prf, in mathcomp.algebra.poly]
    size_poly_exp_leq [prf, in mathcomp.algebra.poly]
    size_poly_gt0 [prf, in mathcomp.algebra.poly]
    size_poly_leq0 [prf, in mathcomp.algebra.poly]
    size_poly_leq0P [prf, in mathcomp.algebra.poly]
    size_poly_prod_leq [prf, in mathcomp.algebra.poly]
    size_poly_XaY [prf, in mathcomp.algebra.polyXY]
    size_poly_XmY [prf, in mathcomp.algebra.polyXY]
    size_polyC [prf, in mathcomp.algebra.poly]
    size_polyC_leq1 [prf, in mathcomp.algebra.poly]
    size_polyD [prf, in mathcomp.algebra.poly]
    size_polyDl [prf, in mathcomp.algebra.poly]
    size_polyMleq [prf, in mathcomp.algebra.poly]
    size_polyN [prf, in mathcomp.algebra.poly]
    size_polyX [prf, in mathcomp.algebra.poly]
    size_polyXn [prf, in mathcomp.algebra.poly]
    size_prefix [prf, in mathcomp.boot.seq]
    size_prod [prf, in mathcomp.algebra.poly]
    size_prod_eq1 [prf, in mathcomp.algebra.poly]
    size_prod_seq [prf, in mathcomp.algebra.poly]
    size_prod_seq_eq1 [prf, in mathcomp.algebra.poly]
    size_prod_XsubC [prf, in mathcomp.algebra.poly]
    size_proper_mul [prf, in mathcomp.algebra.poly]
    size_rat_int_poly [prf, in mathcomp.algebra.rat]
    size_rcons [prf, in mathcomp.boot.seq]
    size_rem [prf, in mathcomp.boot.seq]
    size_reshape [prf, in mathcomp.boot.seq]
    size_rev [prf, in mathcomp.boot.seq]
    size_rot [prf, in mathcomp.boot.seq]
    size_rotr [prf, in mathcomp.boot.seq]
    size_scale [prf, in mathcomp.algebra.poly]
    size_scale_leq [prf, in mathcomp.algebra.poly]
    size_scanl [prf, in mathcomp.boot.seq]
    size_seq_fset [prf, in mathcomp.finmap.finmap]
    size_set_nth [prf, in mathcomp.boot.seq]
    size_sort [prf, in mathcomp.boot.path]
    size_sort_keys [prf, in mathcomp.finmap.finmap]
    size_subseq [prf, in mathcomp.boot.seq]
    size_subseq_leqif [prf, in mathcomp.boot.seq]
    size_suffix [prf, in mathcomp.boot.seq]
    size_sum [prf, in mathcomp.algebra.poly]
    size_take [prf, in mathcomp.boot.seq]
    size_take_min [prf, in mathcomp.boot.seq]
    size_take_poly [prf, in mathcomp.algebra.poly]
    size_takel [prf, in mathcomp.boot.seq]
    size_tally_seq [prf, in mathcomp.boot.seq]
    size_traject [prf, in mathcomp.boot.path]
    size_tuple [prf, in mathcomp.boot.tuple]
    size_undup [prf, in mathcomp.boot.seq]
    size_widen_bseq [prf, in mathcomp.boot.tuple]
    size_XaddC [prf, in mathcomp.algebra.poly]
    size_XmulC [prf, in mathcomp.algebra.poly]
    size_Xn_sub_1 [prf, in mathcomp.algebra.poly]
    size_XnaddC [prf, in mathcomp.algebra.poly]
    size_XnsubC [prf, in mathcomp.algebra.poly]
    size_XsubC [prf, in mathcomp.algebra.poly]
    size_zip [prf, in mathcomp.boot.seq]
    size_zprimitive [prf, in mathcomp.algebra.intdiv]
    sizeY_eq0 [prf, in mathcomp.algebra.polyXY]
    sizeY_mulX [prf, in mathcomp.algebra.polyXY]
    sizeYE [prf, in mathcomp.algebra.polyXY]
    skew_field_algid1 [prf, in mathcomp.field.falgebra]
    skew_field_dimS [prf, in mathcomp.field.falgebra]
    skew_field_module_dimS [prf, in mathcomp.field.falgebra]
    skew_field_module_semisimple [prf, in mathcomp.field.falgebra]
    small_nil_class [prf, in mathcomp.solvable.sylow]
    small_set_sub [prf, in mathcomp.classical.filter]
    smallest_filter_finI [prf, in mathcomp.classical.filter]
    smallest_id [prf, in mathcomp.classical.classical_sets]
    smallest_lambda_system [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_setring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sub [prf, in mathcomp.classical.classical_sets]
    snd_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    snd_is_multiplicative [prf, in mathcomp.boot.monoid]
    snd_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    snd_is_umagma_morphism [prf, in mathcomp.boot.monoid]
    snd_is_zmod_morphism [prf, in mathcomp.boot.nmodule]
    snd_morphM [prf, in mathcomp.finite_group.gproduct]
    snd_open [prf, in mathcomp.analysis.topology_theory.product_topology]
    snd_set_snd [prf, in mathcomp.classical.classical_sets]
    snd_setX [prf, in mathcomp.classical.classical_sets]
    sol_coprime_Sylow_exists [prf, in mathcomp.solvable.hall]
    sol_coprime_Sylow_subset [prf, in mathcomp.solvable.hall]
    sol_coprime_Sylow_trans [prf, in mathcomp.solvable.hall]
    sol_der1_proper [prf, in mathcomp.solvable.nilpotent]
    sol_prime_factor_exists [prf, in mathcomp.solvable.maximal]
    solvable1 [prf, in mathcomp.solvable.nilpotent]
    solvable_AltF [prf, in mathcomp.solvable.alt]
    solvable_norm_abelem [prf, in mathcomp.solvable.maximal]
    solvable_SymF [prf, in mathcomp.solvable.alt]
    solvableS [prf, in mathcomp.solvable.nilpotent]
    solve_Qint_span [prf, in mathcomp.algebra.rat]
    some_big_AC_mk_monoid [prf, in mathcomp.boot.bigop]
    some_big_mk_monoid [prf, in mathcomp.boot.bigop]
    some_bigcap [prf, in mathcomp.classical.classical_sets]
    some_comp_inv [prf, in mathcomp.classical.functions]
    Some_fnd [prf, in mathcomp.finmap.finmap]
    some_image [prf, in mathcomp.classical.classical_sets]
    some_inv [prf, in mathcomp.classical.functions]
    some_iter_inv [prf, in mathcomp.classical.functions]
    Some_oextract [prf, in mathcomp.finmap.finmap]
    Some_ojoin [prf, in mathcomp.finmap.finmap]
    some_preimage [prf, in mathcomp.classical.classical_sets]
    some_set0 [prf, in mathcomp.classical.classical_sets]
    some_set1 [prf, in mathcomp.classical.classical_sets]
    some_set_eq0 [prf, in mathcomp.classical.classical_sets]
    some_setC [prf, in mathcomp.classical.classical_sets]
    some_setD [prf, in mathcomp.classical.classical_sets]
    some_setI [prf, in mathcomp.classical.classical_sets]
    some_setT [prf, in mathcomp.classical.classical_sets]
    some_setU [prf, in mathcomp.classical.classical_sets]
    sop_inj [prf, in mathcomp.solvable.burnside_app]
    sop_morph [prf, in mathcomp.solvable.burnside_app]
    sop_spec [prf, in mathcomp.solvable.burnside_app]
    sort_bseqP [prf, in mathcomp.boot.tuple]
    sort_iota_stable [prf, in mathcomp.boot.path]
    sort_keys_id [prf, in mathcomp.finmap.finmap]
    sort_keys_nil [prf, in mathcomp.finmap.finmap]
    sort_map [prf, in mathcomp.boot.path]
    sort_pairwise_stable [prf, in mathcomp.boot.path]
    sort_sorted [prf, in mathcomp.boot.path]
    sort_sorted_in [prf, in mathcomp.boot.path]
    sort_stable [prf, in mathcomp.boot.path]
    sort_stable_in [prf, in mathcomp.boot.path]
    sort_tupleP [prf, in mathcomp.boot.tuple]
    sort_uniq [prf, in mathcomp.boot.path]
    sortE [prf, in mathcomp.boot.path]
    sorted_cat_cons [prf, in mathcomp.boot.path]
    sorted_divisors [prf, in mathcomp.boot.prime]
    sorted_divisors_ltn [prf, in mathcomp.boot.prime]
    sorted_eq [prf, in mathcomp.boot.path]
    sorted_eq_in [prf, in mathcomp.boot.path]
    sorted_filter [prf, in mathcomp.boot.path]
    sorted_filter_in [prf, in mathcomp.boot.path]
    sorted_leq_index [prf, in mathcomp.boot.path]
    sorted_leq_index_in [prf, in mathcomp.boot.path]
    sorted_leq_nth [prf, in mathcomp.boot.path]
    sorted_leq_nth_in [prf, in mathcomp.boot.path]
    sorted_ltn_index [prf, in mathcomp.boot.path]
    sorted_ltn_index_in [prf, in mathcomp.boot.path]
    sorted_ltn_nth [prf, in mathcomp.boot.path]
    sorted_ltn_nth_in [prf, in mathcomp.boot.path]
    sorted_map [prf, in mathcomp.boot.path]
    sorted_mask [prf, in mathcomp.boot.path]
    sorted_mask_in [prf, in mathcomp.boot.path]
    sorted_mask_sort [prf, in mathcomp.boot.path]
    sorted_mask_sort_in [prf, in mathcomp.boot.path]
    sorted_merge [prf, in mathcomp.boot.path]
    sorted_pairwise [prf, in mathcomp.boot.path]
    sorted_pairwise_in [prf, in mathcomp.boot.path]
    sorted_primes [prf, in mathcomp.boot.prime]
    sorted_relI [prf, in mathcomp.boot.path]
    sorted_sort [prf, in mathcomp.boot.path]
    sorted_sort_in [prf, in mathcomp.boot.path]
    sorted_subseq_sort [prf, in mathcomp.boot.path]
    sorted_subseq_sort_in [prf, in mathcomp.boot.path]
    sorted_uniq [prf, in mathcomp.boot.path]
    sorted_uniq_in [prf, in mathcomp.boot.path]
    sortedP [prf, in mathcomp.boot.path]
    SortKeys.E [prf, in mathcomp.finmap.finmap]
    SortKeys.eq [prf, in mathcomp.finmap.finmap]
    SortKeys.perm [prf, in mathcomp.finmap.finmap]
    SortKeys.uniq [prf, in mathcomp.finmap.finmap]
    span_basis [prf, in mathcomp.algebra.vector]
    span_bigcat [prf, in mathcomp.algebra.vector]
    span_cat [prf, in mathcomp.algebra.vector]
    span_cons [prf, in mathcomp.algebra.vector]
    span_def [prf, in mathcomp.algebra.vector]
    span_key [prf, in mathcomp.algebra.vector]
    span_lfunP [prf, in mathcomp.algebra.vector]
    span_nil [prf, in mathcomp.algebra.vector]
    span_orthogonal [prf, in mathcomp.algebra.sesquilinear]
    span_seq1 [prf, in mathcomp.algebra.vector]
    span_subvP [prf, in mathcomp.algebra.vector]
    spectral_unit [prf, in mathcomp.algebra.spectral]
    spectral_unitarymx [prf, in mathcomp.algebra.spectral]
    split1 [prf, in mathcomp.boot.nmodule]
    split1_extraspecial [prf, in mathcomp.solvable.maximal]
    split_ent_subset [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    split_entP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    split_find [prf, in mathcomp.boot.seq]
    split_find_nth [prf, in mathcomp.boot.seq]
    split_ordP [prf, in mathcomp.boot.fintype]
    splitbij_sub [prf, in mathcomp.classical.functions]
    splitbij_sub_sym [prf, in mathcomp.classical.functions]
    splitid [prf, in mathcomp.classical.functions]
    splitK [prf, in mathcomp.boot.fintype]
    splitP [prf, in mathcomp.boot.path]
    splitP [prf, in mathcomp.boot.fintype]
    splitP2r [prf, in mathcomp.boot.path]
    splitPl [prf, in mathcomp.boot.path]
    splitPr [prf, in mathcomp.boot.path]
    splitsP [prf, in mathcomp.finite_group.gproduct]
    splitting_field_normal [prf, in mathcomp.field.galois]
    splitting_galoisField [prf, in mathcomp.field.galois]
    splitting_normalField [prf, in mathcomp.field.galois]
    splittingFieldForS [prf, in mathcomp.field.galois]
    splittingFieldP [prf, in mathcomp.field.galois]
    splittingPoly [prf, in mathcomp.field.galois]
    splitV [prf, in mathcomp.classical.functions]
    sprob_kernel_le1 [prf, in mathcomp.analysis.kernel]
    sprob_kernelP [prf, in mathcomp.analysis.kernel]
    sprob_mkcomp_noparam [prf, in mathcomp.analysis.kernel]
    sqmx_ind [prf, in mathcomp.algebra.matrix]
    sqr_continuous [prf, in mathcomp.analysis.realfun]
    sqr_sqrte [prf, in mathcomp.reals.constructive_ereal]
    sqre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqreD [prf, in mathcomp.reals.constructive_ereal]
    sqrn_gt0 [prf, in mathcomp.boot.ssrnat]
    sqrn_inj [prf, in mathcomp.boot.ssrnat]
    sqrnB [prf, in mathcomp.boot.ssrnat]
    sqrnD [prf, in mathcomp.boot.ssrnat]
    sqrnD_sub [prf, in mathcomp.boot.ssrnat]
    sqrt_continuous [prf, in mathcomp.analysis.realfun]
    sqrt_dnorm_eq0 [prf, in mathcomp.algebra.sesquilinear]
    sqrt_dnorm_ge0 [prf, in mathcomp.algebra.sesquilinear]
    sqrt_dnorm_gt0 [prf, in mathcomp.algebra.sesquilinear]
    sqrte0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sqrte_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_sqr [prf, in mathcomp.reals.constructive_ereal]
    sqrteM [prf, in mathcomp.reals.constructive_ereal]
    sqrtK [prf, in mathcomp.classical.unstable]
    squeeze_cvge [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    squeeze_cvgr [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    squeeze_fin [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    stab_ntransitive [prf, in mathcomp.solvable.primitive_action]
    stab_ntransitiveI [prf, in mathcomp.solvable.primitive_action]
    stab_semiprime [prf, in mathcomp.solvable.frobenius]
    stable [prf, in mathcomp.solvable.burnside_app]
    stable0mx [prf, in mathcomp.algebra.mxalgebra]
    stableCmx [prf, in mathcomp.algebra.mxalgebra]
    stableDmx [prf, in mathcomp.algebra.mxalgebra]
    stablemx0 [prf, in mathcomp.algebra.mxalgebra]
    stablemx_comp [prf, in mathcomp.algebra.mxred]
    stablemx_comp [prf, in mathcomp.algebra.mxpoly]
    stablemx_full [prf, in mathcomp.algebra.mxalgebra]
    stablemx_restrict [prf, in mathcomp.algebra.mxred]
    stablemx_restrict [prf, in mathcomp.algebra.mxpoly]
    stablemx_row_base [prf, in mathcomp.algebra.mxalgebra]
    stablemx_sums [prf, in mathcomp.algebra.mxalgebra]
    stablemx_unit [prf, in mathcomp.algebra.mxalgebra]
    stablemxC [prf, in mathcomp.algebra.mxalgebra]
    stablemxD [prf, in mathcomp.algebra.mxalgebra]
    stablemxM [prf, in mathcomp.algebra.mxalgebra]
    stablemxN [prf, in mathcomp.algebra.mxalgebra]
    stableNmx [prf, in mathcomp.algebra.mxalgebra]
    start_with_prefix [prf, in mathcomp.classical.classical_orders]
    strace_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Streicher_K__eq_rect_eq [prf, in mathcomp.classical.internal_Eqdep_dec]
    Streicher_K_on__eq_rect_eq_on [prf, in mathcomp.classical.internal_Eqdep_dec]
    strict_adjunction [prf, in mathcomp.boot.fingraph]
    strict_monotonicW [prf, in mathcomp.classical.unstable]
    strictly_dominated_by1 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    strong_Primitive_Element_Theorem [prf, in mathcomp.field.separable]
    strongest_coprime_quotient_cent [prf, in mathcomp.solvable.hall]
    StrongJordanHolderUniqueness [prf, in mathcomp.solvable.jordanholder]
    sub0e [prf, in mathcomp.reals.constructive_ereal]
    sub0mx [prf, in mathcomp.algebra.mxalgebra]
    sub0n [prf, in mathcomp.boot.ssrnat]
    sub0seq [prf, in mathcomp.boot.seq]
    sub0set [prf, in mathcomp.classical.classical_sets]
    sub0set [prf, in mathcomp.boot.finset]
    sub0v [prf, in mathcomp.algebra.vector]
    sub1_agenv [prf, in mathcomp.field.falgebra]
    sub1_scale_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    sub1b [prf, in mathcomp.boot.ssrnat]
    sub1G [prf, in mathcomp.finite_group.fingroup]
    sub1mx [prf, in mathcomp.algebra.mxalgebra]
    sub1seq [prf, in mathcomp.boot.seq]
    sub1set [prf, in mathcomp.classical.classical_sets]
    sub1set [prf, in mathcomp.boot.finset]
    sub1v [prf, in mathcomp.field.fieldext]
    sub_abelian_cent [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_cent2 [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_norm [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_normal [prf, in mathcomp.finite_group.fingroup]
    sub_act_proof [prf, in mathcomp.finite_group.action]
    sub_adds_genmx_ortho [prf, in mathcomp.algebra.spectral]
    sub_addsmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_adjoin1v [prf, in mathcomp.field.fieldext]
    sub_adjoin_separable_generator [prf, in mathcomp.field.separable]
    sub_afixRs_norm [prf, in mathcomp.finite_group.action]
    sub_afixRs_norms [prf, in mathcomp.finite_group.action]
    sub_agenv [prf, in mathcomp.field.falgebra]
    sub_all [prf, in mathcomp.boot.seq]
    sub_allrel [prf, in mathcomp.boot.seq]
    sub_annihilant_in_ideal [prf, in mathcomp.algebra.polyXY]
    sub_annihilant_neq0 [prf, in mathcomp.algebra.polyXY]
    sub_annihilantP [prf, in mathcomp.algebra.polyXY]
    sub_astab1 [prf, in mathcomp.finite_group.action]
    sub_astab1_in [prf, in mathcomp.finite_group.action]
    sub_astabQ [prf, in mathcomp.finite_group.action]
    sub_astabQR [prf, in mathcomp.finite_group.action]
    sub_baseField [prf, in mathcomp.field.fieldext]
    sub_bigcap [prf, in mathcomp.classical.classical_sets]
    sub_bigcapmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_boundedl [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_boundedr [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_capmx [prf, in mathcomp.algebra.mxalgebra]
    sub_capmx_gen [prf, in mathcomp.algebra.mxalgebra]
    sub_caratheodory [prf, in mathcomp.analysis.measure_theory.measure_extension]
    sub_cent1 [prf, in mathcomp.finite_group.fingroup]
    sub_center_normal [prf, in mathcomp.solvable.center]
    sub_class_support [prf, in mathcomp.finite_group.fingroup]
    sub_cofinite_set [prf, in mathcomp.classical.cardinality]
    sub_conjg [prf, in mathcomp.finite_group.fingroup]
    sub_conjgV [prf, in mathcomp.finite_group.fingroup]
    sub_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    sub_cosetpre [prf, in mathcomp.finite_group.quotient]
    sub_cosetpre_quo [prf, in mathcomp.finite_group.quotient]
    sub_count [prf, in mathcomp.boot.seq]
    sub_countable [prf, in mathcomp.classical.cardinality]
    sub_cycle [prf, in mathcomp.boot.path]
    sub_cyclic_char [prf, in mathcomp.solvable.cyclic]
    sub_daddsmx [prf, in mathcomp.algebra.mxalgebra]
    sub_der1_abelian [prf, in mathcomp.solvable.commutator]
    sub_der1_norm [prf, in mathcomp.solvable.commutator]
    sub_der1_normal [prf, in mathcomp.solvable.commutator]
    sub_dominatedl [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_dominatedr [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_double_eseries [prf, in mathcomp.analysis.sequences]
    sub_double_series [prf, in mathcomp.analysis.sequences]
    sub_dsumsmx [prf, in mathcomp.algebra.mxalgebra]
    sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxred]
    sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxpoly]
    sub_eseries [prf, in mathcomp.analysis.sequences]
    sub_eseries_geq [prf, in mathcomp.analysis.sequences]
    sub_find [prf, in mathcomp.boot.seq]
    sub_finite_set [prf, in mathcomp.classical.cardinality]
    sub_g_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_gcore [prf, in mathcomp.finite_group.fingroup]
    sub_gen [prf, in mathcomp.finite_group.fingroup]
    sub_gen_smallest [prf, in mathcomp.classical.classical_sets]
    sub_Hall_pcore [prf, in mathcomp.solvable.pgroup]
    sub_has [prf, in mathcomp.boot.seq]
    sub_im_coset [prf, in mathcomp.finite_group.quotient]
    sub_image_setI [prf, in mathcomp.classical.classical_sets]
    sub_image_some [prf, in mathcomp.classical.classical_sets]
    sub_image_someP [prf, in mathcomp.classical.classical_sets]
    sub_imset_pre [prf, in mathcomp.boot.finset]
    sub_in_allrel [prf, in mathcomp.boot.seq]
    sub_in_constt [prf, in mathcomp.solvable.pgroup]
    sub_in_cycle [prf, in mathcomp.boot.path]
    sub_in_le_big [prf, in mathcomp.boot.bigop]
    sub_in_pairwise [prf, in mathcomp.boot.seq]
    sub_in_partn [prf, in mathcomp.boot.prime]
    sub_in_path [prf, in mathcomp.boot.path]
    sub_in_pcore [prf, in mathcomp.solvable.pgroup]
    sub_in_pnat [prf, in mathcomp.boot.prime]
    sub_in_sorted [prf, in mathcomp.boot.path]
    sub_infinite_set [prf, in mathcomp.classical.cardinality]
    sub_inseparable [prf, in mathcomp.field.separable]
    sub_isog [prf, in mathcomp.finite_group.morphism]
    sub_isom [prf, in mathcomp.finite_group.morphism]
    sub_kermx [prf, in mathcomp.algebra.mxalgebra]
    sub_kermxP [prf, in mathcomp.algebra.mxalgebra]
    sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxred]
    sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxpoly]
    sub_klipschitz [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_lcoset [prf, in mathcomp.finite_group.fingroup]
    sub_lcosetV [prf, in mathcomp.finite_group.fingroup]
    sub_Ldiv [prf, in mathcomp.solvable.abelian]
    sub_LdivT [prf, in mathcomp.solvable.abelian]
    sub_le_big [prf, in mathcomp.boot.bigop]
    sub_le_big_seq [prf, in mathcomp.boot.bigop]
    sub_le_big_seq_cond [prf, in mathcomp.boot.bigop]
    sub_Lfun_finLfun [prf, in mathcomp.analysis.hoelder]
    sub_Lfun_mfun [prf, in mathcomp.analysis.hoelder]
    sub_lipschitz [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_ltmx_trans [prf, in mathcomp.algebra.mxalgebra]
    sub_map [prf, in mathcomp.boot.seq]
    sub_meets [prf, in mathcomp.classical.classical_sets]
    sub_morphim_pre [prf, in mathcomp.finite_group.morphism]
    sub_morphpre_im [prf, in mathcomp.finite_group.morphism]
    sub_morphpre_injm [prf, in mathcomp.finite_group.morphism]
    sub_nilpotent_cent2 [prf, in mathcomp.solvable.sylow]
    sub_normal_Hall [prf, in mathcomp.solvable.pgroup]
    sub_ord_proof [prf, in mathcomp.boot.fintype]
    sub_ordK [prf, in mathcomp.boot.fintype]
    sub_orthonormal [prf, in mathcomp.algebra.sesquilinear]
    sub_p_elt [prf, in mathcomp.solvable.pgroup]
    sub_pairwise [prf, in mathcomp.boot.seq]
    sub_pairwise_orthogonal [prf, in mathcomp.algebra.sesquilinear]
    sub_path [prf, in mathcomp.boot.path]
    sub_pcore [prf, in mathcomp.solvable.pgroup]
    sub_pgroup [prf, in mathcomp.solvable.pgroup]
    sub_pHall [prf, in mathcomp.solvable.pgroup]
    sub_pnat_coprime [prf, in mathcomp.boot.prime]
    sub_proper_trans [prf, in mathcomp.boot.fintype]
    sub_quotient_pre [prf, in mathcomp.finite_group.quotient]
    sub_rcoset [prf, in mathcomp.finite_group.fingroup]
    sub_rcosetV [prf, in mathcomp.finite_group.fingroup]
    sub_Rhull [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_rVP [prf, in mathcomp.algebra.mxalgebra]
    sub_scale_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    sub_series [prf, in mathcomp.analysis.sequences]
    sub_series_geq [prf, in mathcomp.analysis.sequences]
    sub_setP [prf, in mathcomp.classical.cardinality]
    sub_setring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_setring2 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_sfun_fimfun [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sub_sfun_mfun [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sub_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_sigma_algebra2 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_smallest [prf, in mathcomp.classical.classical_sets]
    sub_smallest2l [prf, in mathcomp.classical.classical_sets]
    sub_smallest2r [prf, in mathcomp.classical.classical_sets]
    sub_sorted [prf, in mathcomp.boot.path]
    sub_span [prf, in mathcomp.algebra.vector]
    sub_sums_genmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_sumsmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_trivIset [prf, in mathcomp.classical.classical_sets]
    sub_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    sub_within [prf, in mathcomp.classical.wochoice]
    sub_Zp_1 [prf, in mathcomp.algebra.zmodp]
    subact_is_action [prf, in mathcomp.finite_group.action]
    subBnAC [prf, in mathcomp.boot.ssrnat]
    subcent1_cycle_norm [prf, in mathcomp.solvable.center]
    subcent1_cycle_normal [prf, in mathcomp.solvable.center]
    subcent1_cycle_sub [prf, in mathcomp.solvable.center]
    subcent1_extraspecial_maximal [prf, in mathcomp.solvable.maximal]
    subcent1_id [prf, in mathcomp.solvable.center]
    subcent1_sub [prf, in mathcomp.solvable.center]
    subcent1C [prf, in mathcomp.solvable.center]
    subcent1P [prf, in mathcomp.solvable.center]
    subcent_char [prf, in mathcomp.solvable.center]
    subcent_dprod [prf, in mathcomp.finite_group.gproduct]
    subcent_norm [prf, in mathcomp.solvable.center]
    subcent_normal [prf, in mathcomp.solvable.center]
    subcent_sdprod [prf, in mathcomp.finite_group.gproduct]
    subcent_sub [prf, in mathcomp.solvable.center]
    subcent_TImulg [prf, in mathcomp.finite_group.gproduct]
    subcentP [prf, in mathcomp.solvable.center]
    subclosed_compact [prf, in mathcomp.analysis.topology_theory.compact]
    subCset [prf, in mathcomp.boot.finset]
    subD1set [prf, in mathcomp.boot.finset]
    subDnAC [prf, in mathcomp.boot.ssrnat]
    subDnCA [prf, in mathcomp.boot.ssrnat]
    subDnCAC [prf, in mathcomp.boot.ssrnat]
    subDset [prf, in mathcomp.boot.finset]
    subDsetl [prf, in mathcomp.classical.classical_sets]
    subDsetr [prf, in mathcomp.classical.classical_sets]
    sube0 [prf, in mathcomp.reals.constructive_ereal]
    sube_cvg0 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sube_eq [prf, in mathcomp.reals.constructive_ereal]
    sube_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sube_gt0 [prf, in mathcomp.reals.constructive_ereal]
    sube_le0 [prf, in mathcomp.reals.constructive_ereal]
    sube_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subee [prf, in mathcomp.reals.constructive_ereal]
    subEfproper [prf, in mathcomp.finmap.finmap]
    subeK [prf, in mathcomp.reals.constructive_ereal]
    subEproper [prf, in mathcomp.boot.finset]
    suber_ge0 [prf, in mathcomp.reals.constructive_ereal]
    suber_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subfield_closed [prf, in mathcomp.field.fieldext]
    subfun_imageT [prf, in mathcomp.classical.functions]
    subfun_inj [prf, in mathcomp.classical.functions]
    subfx_eval_is_monoid_morphism [prf, in mathcomp.field.fieldext]
    subfx_eval_is_zmod_morphism [prf, in mathcomp.field.fieldext]
    subfx_evalZ [prf, in mathcomp.field.fieldext]
    subfx_fieldAxiom [prf, in mathcomp.field.fieldext]
    subfx_inj_base [prf, in mathcomp.field.fieldext]
    subfx_inj_eval [prf, in mathcomp.field.fieldext]
    subfx_inj_is_monoid_morphism [prf, in mathcomp.field.fieldext]
    subfx_inj_is_zmod_morphism [prf, in mathcomp.field.fieldext]
    subfx_inj_root [prf, in mathcomp.field.fieldext]
    subfx_injZ [prf, in mathcomp.field.fieldext]
    subfx_inv0 [prf, in mathcomp.field.fieldext]
    subfx_irreducibleP [prf, in mathcomp.field.fieldext]
    subfx_scaleAl [prf, in mathcomp.field.fieldext]
    subfx_scaler1r [prf, in mathcomp.field.fieldext]
    subfx_scalerA [prf, in mathcomp.field.fieldext]
    subfx_scalerDl [prf, in mathcomp.field.fieldext]
    subfx_scalerDr [prf, in mathcomp.field.fieldext]
    subfxE [prf, in mathcomp.field.fieldext]
    subfxEroot [prf, in mathcomp.field.fieldext]
    subG1 [prf, in mathcomp.finite_group.fingroup]
    subG1_contra [prf, in mathcomp.finite_group.fingroup]
    subg_default [prf, in mathcomp.finite_group.fingroup]
    subg_inj [prf, in mathcomp.finite_group.fingroup]
    subg_invP [prf, in mathcomp.finite_group.fingroup]
    subg_mulP [prf, in mathcomp.finite_group.fingroup]
    subg_oneP [prf, in mathcomp.finite_group.fingroup]
    subgacent1E [prf, in mathcomp.finite_group.action]
    subgacentE [prf, in mathcomp.finite_group.action]
    subgK [prf, in mathcomp.finite_group.fingroup]
    subgM [prf, in mathcomp.finite_group.fingroup]
    subgmK [prf, in mathcomp.finite_group.morphism]
    subgP [prf, in mathcomp.finite_group.fingroup]
    subgroup_transitiveP [prf, in mathcomp.finite_group.action]
    subgroup_transitivePin [prf, in mathcomp.finite_group.action]
    subHall_Hall [prf, in mathcomp.solvable.pgroup]
    subHall_Sylow [prf, in mathcomp.solvable.pgroup]
    subimageK [prf, in mathcomp.classical.classical_sets]
    subIset [prf, in mathcomp.classical.classical_sets]
    subIset [prf, in mathcomp.boot.finset]
    subIsetl [prf, in mathcomp.classical.classical_sets]
    subIsetr [prf, in mathcomp.classical.classical_sets]
    subitv_anti [prf, in mathcomp.algebra.interval]
    subitv_refl [prf, in mathcomp.algebra.interval]
    subitv_trans [prf, in mathcomp.algebra.interval]
    subitvE [prf, in mathcomp.algebra.interval]
    subitvP [prf, in mathcomp.algebra.interval]
    subitvPl [prf, in mathcomp.algebra.interval]
    subitvPr [prf, in mathcomp.algebra.interval]
    SubK [prf, in mathcomp.boot.eqtype]
    subKimage [prf, in mathcomp.classical.classical_sets]
    subKn [prf, in mathcomp.boot.ssrnat]
    subl_surj [prf, in mathcomp.classical.functions]
    submx0 [prf, in mathcomp.algebra.mxalgebra]
    submx0null [prf, in mathcomp.algebra.mxalgebra]
    submx1 [prf, in mathcomp.algebra.mxalgebra]
    submx_full [prf, in mathcomp.algebra.mxalgebra]
    submx_ortho [prf, in mathcomp.algebra.spectral]
    submx_refl [prf, in mathcomp.algebra.mxalgebra]
    submx_rowsub [prf, in mathcomp.algebra.mxalgebra]
    submx_trans [prf, in mathcomp.algebra.mxalgebra]
    submxblock0 [prf, in mathcomp.algebra.matrix]
    submxblock_diag [prf, in mathcomp.algebra.matrix]
    submxblock_sum [prf, in mathcomp.algebra.matrix]
    submxblockB [prf, in mathcomp.algebra.matrix]
    submxblockD [prf, in mathcomp.algebra.matrix]
    submxblockEh [prf, in mathcomp.algebra.matrix]
    submxblockEv [prf, in mathcomp.algebra.matrix]
    submxblockK [prf, in mathcomp.algebra.matrix]
    submxblockN [prf, in mathcomp.algebra.matrix]
    submxcol0 [prf, in mathcomp.algebra.matrix]
    submxcol_matrix [prf, in mathcomp.algebra.matrix]
    submxcol_mul [prf, in mathcomp.algebra.matrix]
    submxcol_sum [prf, in mathcomp.algebra.matrix]
    submxcolB [prf, in mathcomp.algebra.matrix]
    submxcolD [prf, in mathcomp.algebra.matrix]
    submxcolK [prf, in mathcomp.algebra.matrix]
    submxcolN [prf, in mathcomp.algebra.matrix]
    submxE [prf, in mathcomp.algebra.mxalgebra]
    submxElt [prf, in mathcomp.algebra.mxalgebra]
    submxK [prf, in mathcomp.algebra.matrix]
    submxMfree [prf, in mathcomp.algebra.mxalgebra]
    submxMl [prf, in mathcomp.algebra.mxalgebra]
    submxMr [prf, in mathcomp.algebra.mxalgebra]
    submxP [prf, in mathcomp.algebra.mxalgebra]
    submxrow0 [prf, in mathcomp.algebra.matrix]
    submxrow_matrix [prf, in mathcomp.algebra.matrix]
    submxrow_sum [prf, in mathcomp.algebra.matrix]
    submxrowB [prf, in mathcomp.algebra.matrix]
    submxrowD [prf, in mathcomp.algebra.matrix]
    submxrowK [prf, in mathcomp.algebra.matrix]
    submxrowN [prf, in mathcomp.algebra.matrix]
    subn0 [prf, in mathcomp.boot.ssrnat]
    subn1 [prf, in mathcomp.boot.ssrnat]
    subn2 [prf, in mathcomp.boot.ssrnat]
    subn_eq0 [prf, in mathcomp.boot.ssrnat]
    subn_exp [prf, in mathcomp.boot.binomial]
    subn_gt0 [prf, in mathcomp.boot.ssrnat]
    subn_if_gt [prf, in mathcomp.boot.ssrnat]
    subn_maxl [prf, in mathcomp.boot.ssrnat]
    subn_minl [prf, in mathcomp.boot.ssrnat]
    subn_sqr [prf, in mathcomp.boot.ssrnat]
    subnA [prf, in mathcomp.boot.ssrnat]
    subnAC [prf, in mathcomp.boot.ssrnat]
    subnBA [prf, in mathcomp.boot.ssrnat]
    subnBAC [prf, in mathcomp.boot.ssrnat]
    subnBl_leq [prf, in mathcomp.boot.ssrnat]
    subnBr_leq [prf, in mathcomp.boot.ssrnat]
    subnCBA [prf, in mathcomp.boot.ssrnat]
    subnDA [prf, in mathcomp.boot.ssrnat]
    subnDAC [prf, in mathcomp.boot.ssrnat]
    subnDl [prf, in mathcomp.boot.ssrnat]
    subnDr [prf, in mathcomp.boot.ssrnat]
    subnE [prf, in mathcomp.boot.ssrnat]
    subnK [prf, in mathcomp.boot.ssrnat]
    subnKC [prf, in mathcomp.boot.ssrnat]
    subnn [prf, in mathcomp.boot.ssrnat]
    subnormal_refl [prf, in mathcomp.solvable.gseries]
    subnormal_sub [prf, in mathcomp.solvable.gseries]
    subnormal_trans [prf, in mathcomp.solvable.gseries]
    subnormalEl [prf, in mathcomp.solvable.gseries]
    subnormalEr [prf, in mathcomp.solvable.gseries]
    subnormalEsupport [prf, in mathcomp.solvable.gseries]
    subnormalP [prf, in mathcomp.solvable.gseries]
    subnS [prf, in mathcomp.boot.ssrnat]
    subnSK [prf, in mathcomp.boot.ssrnat]
    SubP [prf, in mathcomp.boot.eqtype]
    subq_ge0 [prf, in mathcomp.algebra.rat]
    subr_cvg0 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subr_surj [prf, in mathcomp.classical.functions]
    subre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    subre_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subrKC [prf, in mathcomp.classical.mathcomp_extra]
    subseq0 [prf, in mathcomp.boot.seq]
    subseq_anti [prf, in mathcomp.boot.seq]
    subseq_cat2l [prf, in mathcomp.boot.seq]
    subseq_cat2r [prf, in mathcomp.boot.seq]
    subseq_cons [prf, in mathcomp.boot.seq]
    subseq_filter [prf, in mathcomp.boot.seq]
    subseq_pairwise [prf, in mathcomp.boot.seq]
    subseq_path [prf, in mathcomp.boot.path]
    subseq_path_in [prf, in mathcomp.boot.path]
    subseq_rcons [prf, in mathcomp.boot.seq]
    subseq_refl [prf, in mathcomp.boot.seq]
    subseq_rem [prf, in mathcomp.boot.seq]
    subseq_rev [prf, in mathcomp.boot.seq]
    subseq_rot [prf, in mathcomp.boot.seq]
    subseq_sort [prf, in mathcomp.boot.path]
    subseq_sort_in [prf, in mathcomp.boot.path]
    subseq_sorted [prf, in mathcomp.boot.path]
    subseq_sorted_in [prf, in mathcomp.boot.path]
    subseq_trans [prf, in mathcomp.boot.seq]
    subseq_uniq [prf, in mathcomp.boot.seq]
    subseq_uniqP [prf, in mathcomp.boot.seq]
    subseqP [prf, in mathcomp.boot.seq]
    subset0 [prf, in mathcomp.classical.classical_sets]
    subset0 [prf, in mathcomp.boot.finset]
    subset1 [prf, in mathcomp.boot.finset]
    subset_all [prf, in mathcomp.boot.fintype]
    subset_ball_prop_in_itv [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_ball_prop_in_itvcc [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_bigcap [prf, in mathcomp.classical.classical_sets]
    subset_bigcap_r [prf, in mathcomp.classical.classical_sets]
    subset_bigcup [prf, in mathcomp.classical.classical_sets]
    subset_bigcup_r [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI_cond [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU_cond [prf, in mathcomp.classical.classical_sets]
    subset_card_le [prf, in mathcomp.classical.cardinality]
    subset_cardP [prf, in mathcomp.boot.fintype]
    subset_cat2 [prf, in mathcomp.boot.fintype]
    subset_catl [prf, in mathcomp.boot.fintype]
    subset_catr [prf, in mathcomp.boot.fintype]
    subset_closed_ball [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subset_closure [prf, in mathcomp.boot.fingraph]
    subset_closure [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_closure_half [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subset_cons [prf, in mathcomp.boot.seq]
    subset_cons [prf, in mathcomp.boot.fintype]
    subset_cons2 [prf, in mathcomp.boot.seq]
    subset_cons2 [prf, in mathcomp.boot.fintype]
    subset_cover [prf, in mathcomp.boot.finset]
    subset_dfs [prf, in mathcomp.boot.fingraph]
    subset_disjoint [prf, in mathcomp.boot.fintype]
    subset_eqP [prf, in mathcomp.boot.fintype]
    subset_faithful [prf, in mathcomp.finite_group.action]
    subset_filter [prf, in mathcomp.boot.fintype]
    subset_filter_proper [prf, in mathcomp.classical.filter]
    subset_fst_set [prf, in mathcomp.classical.classical_sets]
    subset_fsub [prf, in mathcomp.finmap.finmap]
    subset_fsubE [prf, in mathcomp.finmap.finmap]
    subset_gen [prf, in mathcomp.finite_group.fingroup]
    subset_has_lbound [prf, in mathcomp.classical.classical_sets]
    subset_has_ubound [prf, in mathcomp.classical.classical_sets]
    subset_imfset [prf, in mathcomp.finmap.finmap]
    subset_iter [prf, in mathcomp.boot.finset]
    subset_iterS [prf, in mathcomp.boot.finset]
    subset_itv [prf, in mathcomp.classical.set_interval]
    subset_itv [prf, in mathcomp.algebra.interval]
    subset_itv_bound [prf, in mathcomp.algebra.interval]
    subset_itv_co_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oc_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oo_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oo_co [prf, in mathcomp.algebra.interval]
    subset_itv_oo_oc [prf, in mathcomp.algebra.interval]
    subset_itvl [prf, in mathcomp.classical.set_interval]
    subset_itvP [prf, in mathcomp.classical.set_interval]
    subset_itvr [prf, in mathcomp.classical.set_interval]
    subset_itvScc [prf, in mathcomp.classical.set_interval]
    subset_itvSoo [prf, in mathcomp.classical.set_interval]
    subset_itvW [prf, in mathcomp.classical.set_interval]
    subset_le_big [prf, in mathcomp.boot.bigop]
    subset_le_big_cond [prf, in mathcomp.boot.finset]
    subset_lee_nneseries [prf, in mathcomp.analysis.sequences]
    subset_leq_card [prf, in mathcomp.boot.fintype]
    subset_leqif_card [prf, in mathcomp.boot.fintype]
    subset_leqif_cards [prf, in mathcomp.boot.finset]
    subset_limgP [prf, in mathcomp.algebra.vector]
    subset_limit_point [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_mapP [prf, in mathcomp.boot.seq]
    subset_measure0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    subset_memP [prf, in mathcomp.boot.seq]
    subset_msetBLR [prf, in mathcomp.finmap.multiset]
    subset_neq0 [prf, in mathcomp.boot.finset]
    subset_nonempty [prf, in mathcomp.classical.classical_sets]
    subset_null_set [prf, in mathcomp.analysis.measure_theory.measure_negligible]
    subset_pred1 [prf, in mathcomp.boot.fintype]
    subset_predT [prf, in mathcomp.boot.fintype]
    subset_refl [prf, in mathcomp.classical.classical_sets]
    subset_seqDU [prf, in mathcomp.analysis.sequences]
    subset_set1 [prf, in mathcomp.classical.classical_sets]
    subset_set2 [prf, in mathcomp.classical.classical_sets]
    subset_snd_set [prf, in mathcomp.classical.classical_sets]
    subset_split_ent [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    subset_strace [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    subset_trans [prf, in mathcomp.classical.classical_sets]
    subset_trans [prf, in mathcomp.boot.fintype]
    subsetC [prf, in mathcomp.classical.classical_sets]
    subsetC [prf, in mathcomp.boot.finset]
    subsetC1 [prf, in mathcomp.classical.classical_sets]
    subsetC2 [prf, in mathcomp.classical.classical_sets]
    subsetC_disjoint [prf, in mathcomp.boot.finset]
    subsetC_trivIset [prf, in mathcomp.classical.classical_sets]
    subsetCl [prf, in mathcomp.classical.classical_sets]
    subsetCP [prf, in mathcomp.classical.classical_sets]
    subsetCPl [prf, in mathcomp.classical.classical_sets]
    subsetCPr [prf, in mathcomp.classical.classical_sets]
    subsetCr [prf, in mathcomp.classical.classical_sets]
    subsetD [prf, in mathcomp.boot.finset]
    subsetD1 [prf, in mathcomp.boot.finset]
    subsetD1P [prf, in mathcomp.boot.finset]
    subsetDl [prf, in mathcomp.boot.finset]
    subsetDP [prf, in mathcomp.boot.finset]
    subsetDr [prf, in mathcomp.boot.finset]
    subsetE [prf, in mathcomp.boot.fintype]
    subsetI [prf, in mathcomp.classical.classical_sets]
    subsetI [prf, in mathcomp.boot.finset]
    subsetI_eq0 [prf, in mathcomp.classical.classical_sets]
    subsetI_neq0 [prf, in mathcomp.classical.classical_sets]
    subsetIidl [prf, in mathcomp.boot.finset]
    subsetIidr [prf, in mathcomp.boot.finset]
    subsetIl [prf, in mathcomp.boot.finset]
    subsetIP [prf, in mathcomp.boot.finset]
    subsetIr [prf, in mathcomp.boot.finset]
    subsetP [prf, in mathcomp.classical.classical_sets]
    subsetP [prf, in mathcomp.boot.fintype]
    subsetPn [prf, in mathcomp.boot.fintype]
    subsets_disjoint [prf, in mathcomp.classical.classical_sets]
    subsets_disjoint [prf, in mathcomp.boot.finset]
    subsetT [prf, in mathcomp.classical.classical_sets]
    subsetT [prf, in mathcomp.boot.finset]
    subsetT_hint [prf, in mathcomp.boot.finset]
    subsetU [prf, in mathcomp.boot.finset]
    subsetU1 [prf, in mathcomp.boot.finset]
    subsetUl [prf, in mathcomp.classical.classical_sets]
    subsetUl [prf, in mathcomp.boot.finset]
    subsetUr [prf, in mathcomp.classical.classical_sets]
    subsetUr [prf, in mathcomp.boot.finset]
    subsetW [prf, in mathcomp.classical.classical_sets]
    subSKn [prf, in mathcomp.boot.ssrnat]
    subSn [prf, in mathcomp.boot.ssrnat]
    subSnn [prf, in mathcomp.boot.ssrnat]
    subspace_continuous_measurable_fun [prf, in mathcomp.analysis.measurable_realfun]
    subspace_continuousP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_cvgP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_eq_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    subspace_sigL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_subtypeP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_valL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_valL_continuousP' [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspaceT_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subSS [prf, in mathcomp.boot.ssrnat]
    subTset [prf, in mathcomp.classical.classical_sets]
    subTset [prf, in mathcomp.boot.finset]
    subUset [prf, in mathcomp.classical.classical_sets]
    subUset [prf, in mathcomp.boot.finset]
    subUsetP [prf, in mathcomp.boot.finset]
    subv0 [prf, in mathcomp.algebra.vector]
    subv_add [prf, in mathcomp.algebra.vector]
    subv_adjoin [prf, in mathcomp.field.falgebra]
    subv_adjoin_seq [prf, in mathcomp.field.falgebra]
    subv_anti [prf, in mathcomp.algebra.vector]
    subv_bigcapP [prf, in mathcomp.algebra.vector]
    subv_cap [prf, in mathcomp.algebra.vector]
    subv_cent1 [prf, in mathcomp.field.falgebra]
    subv_sumP [prf, in mathcomp.algebra.vector]
    subv_trans [prf, in mathcomp.algebra.vector]
    subvf [prf, in mathcomp.algebra.vector]
    subvP [prf, in mathcomp.algebra.vector]
    subvP_adjoin [prf, in mathcomp.field.falgebra]
    subvPn [prf, in mathcomp.algebra.vector]
    subvs_fieldMixin [prf, in mathcomp.field.fieldext]
    subvs_inj [prf, in mathcomp.algebra.vector]
    subvs_mu1l [prf, in mathcomp.field.falgebra]
    subvs_mul1 [prf, in mathcomp.field.falgebra]
    subvs_mulA [prf, in mathcomp.field.falgebra]
    subvs_mulDl [prf, in mathcomp.field.falgebra]
    subvs_mulDr [prf, in mathcomp.field.falgebra]
    subvs_scaleAl [prf, in mathcomp.field.falgebra]
    subvs_scaleAr [prf, in mathcomp.field.falgebra]
    subvs_vect_iso [prf, in mathcomp.algebra.vector]
    SubvsE [prf, in mathcomp.algebra.vector]
    subvsP [prf, in mathcomp.algebra.vector]
    subvv [prf, in mathcomp.algebra.vector]
    subX_agenv [prf, in mathcomp.field.falgebra]
    subxx [prf, in mathcomp.boot.fintype]
    subxx_hint [prf, in mathcomp.boot.fintype]
    subzn [prf, in mathcomp.algebra.ssrint]
    subzSS [prf, in mathcomp.algebra.ssrint]
    succn_inj [prf, in mathcomp.boot.ssrnat]
    succnK [prf, in mathcomp.boot.ssrnat]
    suffix0s [prf, in mathcomp.boot.seq]
    suffix1s [prf, in mathcomp.boot.seq]
    suffix_catl [prf, in mathcomp.boot.seq]
    suffix_catr [prf, in mathcomp.boot.seq]
    suffix_cons [prf, in mathcomp.boot.seq]
    suffix_drop [prf, in mathcomp.boot.seq]
    suffix_infix [prf, in mathcomp.boot.seq]
    suffix_infix_trans [prf, in mathcomp.boot.seq]
    suffix_prefix_trans [prf, in mathcomp.boot.seq]
    suffix_rcons [prf, in mathcomp.boot.seq]
    suffix_refl [prf, in mathcomp.boot.seq]
    suffix_rev [prf, in mathcomp.boot.seq]
    suffix_revLR [prf, in mathcomp.boot.seq]
    suffix_sorted [prf, in mathcomp.boot.path]
    suffix_subseq [prf, in mathcomp.boot.seq]
    suffix_suffix [prf, in mathcomp.boot.seq]
    suffix_trans [prf, in mathcomp.boot.seq]
    suffix_uniq [prf, in mathcomp.boot.seq]
    suffixE [prf, in mathcomp.boot.seq]
    suffixP [prf, in mathcomp.boot.seq]
    suffixs0 [prf, in mathcomp.boot.seq]
    suffixW [prf, in mathcomp.boot.seq]
    sum1_card [prf, in mathcomp.boot.bigop]
    sum1_count [prf, in mathcomp.boot.bigop]
    sum1_size [prf, in mathcomp.boot.bigop]
    sum1dep_card [prf, in mathcomp.boot.finset]
    sum_card_class [prf, in mathcomp.finite_group.action]
    sum_drop_poly [prf, in mathcomp.algebra.poly]
    sum_enum_prob [prf, in mathcomp.analysis.probability_theory.random_variable]
    sum_enum_uniq [prf, in mathcomp.boot.fintype]
    sum_eqE [prf, in mathcomp.boot.eqtype]
    sum_eqP [prf, in mathcomp.boot.eqtype]
    sum_even_poly [prf, in mathcomp.algebra.poly]
    sum_ffun [prf, in mathcomp.boot.nmodule]
    sum_ffun [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    sum_ffunE [prf, in mathcomp.boot.nmodule]
    sum_ffunE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    sum_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sum_fin_numP [prf, in mathcomp.reals.constructive_ereal]
    sum_fine [prf, in mathcomp.reals.constructive_ereal]
    sum_index_rcosets_cycle [prf, in mathcomp.solvable.finmodule]
    sum_lfunE [prf, in mathcomp.algebra.vector]
    sum_mset [prf, in mathcomp.finmap.multiset]
    sum_nat_cond_const [prf, in mathcomp.boot.finset]
    sum_nat_const [prf, in mathcomp.boot.bigop]
    sum_nat_const_nat [prf, in mathcomp.boot.bigop]
    sum_nat_eq0 [prf, in mathcomp.boot.bigop]
    sum_nat_eq1 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_eq0 [prf, in mathcomp.finmap.multiset]
    sum_nat_seq_eq0 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_eq1 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_neq0 [prf, in mathcomp.boot.bigop]
    sum_ncycle_totient [prf, in mathcomp.solvable.cyclic]
    sum_nnsfunE [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sum_odd_poly [prf, in mathcomp.algebra.poly]
    sum_totient_dvd [prf, in mathcomp.solvable.cyclic]
    sume_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sume_le0 [prf, in mathcomp.reals.constructive_ereal]
    sumEFin [prf, in mathcomp.reals.constructive_ereal]
    sumeN [prf, in mathcomp.reals.constructive_ereal]
    sumfv [prf, in mathcomp.algebra.vector]
    summable_cvg [prf, in mathcomp.analysis.esum]
    summable_eseries [prf, in mathcomp.analysis.esum]
    summable_eseries_esum [prf, in mathcomp.analysis.esum]
    summable_fine_sum [prf, in mathcomp.analysis.esum]
    summable_funeneg [prf, in mathcomp.analysis.esum]
    summable_funepos [prf, in mathcomp.analysis.esum]
    summable_integral_dirac [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
    summable_nneseries_lim [prf, in mathcomp.analysis.esum]
    summable_pinfty [prf, in mathcomp.analysis.esum]
    summableB [prf, in mathcomp.analysis.esum]
    summableD [prf, in mathcomp.analysis.esum]
    summableE [prf, in mathcomp.analysis.esum]
    summableN [prf, in mathcomp.analysis.esum]
    summx_sub [prf, in mathcomp.algebra.mxalgebra]
    summx_sub_sums [prf, in mathcomp.algebra.mxalgebra]
    summxE [prf, in mathcomp.algebra.matrix]
    sumMz [prf, in mathcomp.algebra.ssrint]
    sumn_cat [prf, in mathcomp.boot.seq]
    sumn_count [prf, in mathcomp.boot.seq]
    sumn_filter [prf, in mathcomp.finmap.multiset]
    sumn_flatten [prf, in mathcomp.boot.seq]
    sumn_map [prf, in mathcomp.finmap.multiset]
    sumn_map_filter [prf, in mathcomp.finmap.multiset]
    sumn_ncons [prf, in mathcomp.boot.seq]
    sumn_nseq [prf, in mathcomp.boot.seq]
    sumn_rcons [prf, in mathcomp.boot.seq]
    sumn_rev [prf, in mathcomp.boot.seq]
    sumn_rot [prf, in mathcomp.boot.seq]
    sumn_set_nth [prf, in mathcomp.boot.seq]
    sumn_set_nth0 [prf, in mathcomp.boot.seq]
    sumn_set_nth_ltn [prf, in mathcomp.boot.seq]
    sumnB [prf, in mathcomp.boot.bigop]
    sumnE [prf, in mathcomp.boot.bigop]
    sumr_le0 [prf, in mathcomp.classical.mathcomp_extra]
    sumrfctE [prf, in mathcomp.classical.functions]
    sumsmx_subP [prf, in mathcomp.algebra.mxalgebra]
    sumsmx_sup [prf, in mathcomp.algebra.mxalgebra]
    sumsmxMr [prf, in mathcomp.algebra.mxalgebra]
    sumsmxMr_gen [prf, in mathcomp.algebra.mxalgebra]
    sumsmxS [prf, in mathcomp.algebra.mxalgebra]
    sumv_pi_nat_sum [prf, in mathcomp.algebra.vector]
    sumv_pi_sum [prf, in mathcomp.algebra.vector]
    sumv_pi_uniq_sum [prf, in mathcomp.algebra.vector]
    sumv_sup [prf, in mathcomp.algebra.vector]
    sup0 [prf, in mathcomp.reals.reals]
    sup1 [prf, in mathcomp.reals.reals]
    sup_adherent [prf, in mathcomp.reals.reals]
    sup_contract_le1 [prf, in mathcomp.analysis.ereal]
    sup_down [prf, in mathcomp.reals.reals]
    sup_ent_filter [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_inv [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_nbhs [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_refl [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_split [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_field_module [prf, in mathcomp.field.fieldext]
    sup_gt [prf, in mathcomp.reals.reals]
    sup_in_floor_set [prf, in mathcomp.reals.reals]
    sup_itv [prf, in mathcomp.reals.real_interval]
    sup_itvcc [prf, in mathcomp.reals.real_interval]
    sup_le [prf, in mathcomp.reals.reals]
    sup_out [prf, in mathcomp.reals.reals]
    sup_setU [prf, in mathcomp.reals.reals]
    sup_sumE [prf, in mathcomp.reals.reals]
    sup_total [prf, in mathcomp.reals.reals]
    sup_ub_strict [prf, in mathcomp.reals.reals]
    sup_upper_bound [prf, in mathcomp.reals.reals]
    super_bij [prf, in mathcomp.classical.cardinality]
    supportE [prf, in mathcomp.boot.finfun]
    supportP [prf, in mathcomp.boot.finfun]
    supremum0 [prf, in mathcomp.classical.classical_sets]
    supremum1 [prf, in mathcomp.classical.classical_sets]
    supremum_out [prf, in mathcomp.classical.classical_sets]
    supremum_pinfty [prf, in mathcomp.analysis.ereal]
    supremums1 [prf, in mathcomp.classical.classical_sets]
    supremumsT [prf, in mathcomp.analysis.ereal]
    supremumT [prf, in mathcomp.analysis.ereal]
    sups_preimage [prf, in mathcomp.analysis.sequences]
    supsN [prf, in mathcomp.analysis.sequences]
    surj [prf, in mathcomp.classical.functions]
    surj_card_ge [prf, in mathcomp.classical.cardinality]
    surj_comp [prf, in mathcomp.classical.functions]
    surj_epi [prf, in mathcomp.classical.functions]
    surj_id [prf, in mathcomp.classical.functions]
    surj_image_eq [prf, in mathcomp.classical.functions]
    surj_set0 [prf, in mathcomp.classical.functions]
    surjE [prf, in mathcomp.classical.functions]
    surjective_existT [prf, in mathcomp.classical.boolp]
    surjective_oinvK [prf, in mathcomp.classical.functions]
    surjective_oinvS [prf, in mathcomp.classical.functions]
    surjfunPex [prf, in mathcomp.classical.cardinality]
    surjPex [prf, in mathcomp.classical.cardinality]
    surjPfun [prf, in mathcomp.classical.functions]
    surjpinv_bij [prf, in mathcomp.classical.functions]
    surjpinv_image_sub [prf, in mathcomp.classical.functions]
    surjpinv_inj [prf, in mathcomp.classical.functions]
    surjpK [prf, in mathcomp.classical.functions]
    Sv_inj [prf, in mathcomp.solvable.burnside_app]
    sv_inv [prf, in mathcomp.solvable.burnside_app]
    swap_continuous [prf, in mathcomp.analysis.topology_theory.product_topology]
    swap_pairK [prf, in mathcomp.boot.ssrfun]
    swapK [prf, in mathcomp.classical.unstable]
    swapXY_comp_poly [prf, in mathcomp.algebra.polyXY]
    swapXY_eq0 [prf, in mathcomp.algebra.polyXY]
    swapXY_is_monoid_morphism [prf, in mathcomp.algebra.polyXY]
    swapXY_is_scalable [prf, in mathcomp.algebra.polyXY]
    swapXY_is_zmod_morphism [prf, in mathcomp.algebra.polyXY]
    swapXY_key [prf, in mathcomp.algebra.polyXY]
    swapXY_map [prf, in mathcomp.algebra.polyXY]
    swapXY_map_polyC [prf, in mathcomp.algebra.polyXY]
    swapXY_poly_XaY [prf, in mathcomp.algebra.polyXY]
    swapXY_poly_XmY [prf, in mathcomp.algebra.polyXY]
    swapXY_polyC [prf, in mathcomp.algebra.polyXY]
    swapXY_X [prf, in mathcomp.algebra.polyXY]
    swapXY_Y [prf, in mathcomp.algebra.polyXY]
    swapXYK [prf, in mathcomp.algebra.polyXY]
    swizzle_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
    swizzle_mx_is_scalable [prf, in mathcomp.algebra.matrix]
    swizzle_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
    Syl_trans [prf, in mathcomp.solvable.sylow]
    Sylow's_theorem [prf, in mathcomp.solvable.sylow]
    Sylow1 [prf, in mathcomp.solvable.pgroup]
    Sylow_exists [prf, in mathcomp.solvable.sylow]
    Sylow_gen [prf, in mathcomp.solvable.sylow]
    Sylow_Jsub [prf, in mathcomp.solvable.sylow]
    Sylow_setI_normal [prf, in mathcomp.solvable.sylow]
    Sylow_subJ [prf, in mathcomp.solvable.sylow]
    Sylow_subnorm [prf, in mathcomp.solvable.sylow]
    Sylow_superset [prf, in mathcomp.solvable.sylow]
    Sylow_trans [prf, in mathcomp.solvable.sylow]
    Sylow_transversal_gen [prf, in mathcomp.solvable.sylow]
    SylowJ [prf, in mathcomp.solvable.pgroup]
    SylowP [prf, in mathcomp.solvable.pgroup]
    Sylvester_mxE [prf, in mathcomp.algebra.mxpoly]
    sym_connect_sym [prf, in mathcomp.boot.fingraph]
    Sym_group_set [prf, in mathcomp.finite_group.perm]
    Sym_trans [prf, in mathcomp.solvable.alt]
    SymE [prf, in mathcomp.finite_group.action]
    symmetric_normalmx [prf, in mathcomp.algebra.spectral]
    symplectic_type_group_structure [prf, in mathcomp.solvable.extremal]
    Generated by rocqnavi