Global Index

J

K

Y

Z

_

(1044 entries)

Variable Index

G

J

K

N

O

Q

R

V

W

X

Y

Z

_

other

(60 entries)

Library Index

G

H

J

K

L

N

R

T

U

V

W

X

Y

Z

_

other

(31 entries)

Lemma Index

J

K

Y

Z

_

other

(704 entries)

Constructor Index

A

B

F

G

H

I

J

K

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Section Index

G

J

K

N

O

Q

R

V

W

X

Y

Z

_

other

(42 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

R

T

U

V

W

X

Y

Z

_

(3 entries)

Definition Index

G

J

K

N

X

Y

Z

_

other

(197 entries)

Global Index

A

all_D_transitions [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
all_bnd_apply_psis [lemma, in mathcomp_eulerian.perm_seq_bridge]
all_le_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
AltDesc [section, in mathcomp_eulerian.altsub]
AltDesc.n [variable, in mathcomp_eulerian.altsub]
altsub [library]
alt_pair_parity [lemma, in mathcomp_eulerian.beta_swap]
alt_desc_set_is_alt [lemma, in mathcomp_eulerian.beta_swap]
alt_desc_set [definition, in mathcomp_eulerian.beta_swap]
alt_aux_from_sign [lemma, in mathcomp_eulerian.altsub]
alt_aux_size_ge1 [lemma, in mathcomp_eulerian.altsub]
alt_aux_cons [lemma, in mathcomp_eulerian.altsub]
alt_321_sub [definition, in mathcomp_eulerian.altsub]
alt_31425 [definition, in mathcomp_eulerian.altsub]
alt_3142 [definition, in mathcomp_eulerian.altsub]
alt_321 [definition, in mathcomp_eulerian.altsub]
alt_312 [definition, in mathcomp_eulerian.altsub]
alt_aux [definition, in mathcomp_eulerian.altsub]
apply_psis_rcons [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_cat [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_cons [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_nil [lemma, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis [definition, in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_size_eq [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_cancel [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_revK [lemma, in mathcomp_eulerian.perm_seq_bridge]
apply_psis_rev [lemma, in mathcomp_eulerian.perm_seq_bridge]
asc [definition, in mathcomp_eulerian.descent]
AsPermMaxBounds [section, in mathcomp_eulerian.altsub]
AsPermMaxBoundsM [section, in mathcomp_eulerian.altsub]
AsPermMaxBoundsM.n [variable, in mathcomp_eulerian.altsub]
AsPermMaxBounds.n [variable, in mathcomp_eulerian.altsub]
as_perm_max_eq [lemma, in mathcomp_eulerian.altsub]
as_perm_max_upper [lemma, in mathcomp_eulerian.altsub]
as_perm_max_lower [lemma, in mathcomp_eulerian.altsub]
as_perm_max_full [lemma, in mathcomp_eulerian.altsub]
as_perm_max_le_size [lemma, in mathcomp_eulerian.altsub]
as_perm_full [lemma, in mathcomp_eulerian.altsub]
as_perm_max_ge0 [lemma, in mathcomp_eulerian.altsub]
as_perm_alt_desc [lemma, in mathcomp_eulerian.altsub]
as_perm_id [lemma, in mathcomp_eulerian.altsub]
as_perm_le_size [lemma, in mathcomp_eulerian.altsub]
as_perm_ge2 [lemma, in mathcomp_eulerian.altsub]
as_permE [lemma, in mathcomp_eulerian.altsub]
as_perm [definition, in mathcomp_eulerian.altsub]
as_perm_max [definition, in mathcomp_eulerian.altsub]
aux_id [lemma, in mathcomp_eulerian.eulerian]
aux_id_step [lemma, in mathcomp_eulerian.eulerian]

B

beta [definition, in mathcomp_eulerian.beta]
beta [library]
beta_alt_max [lemma, in mathcomp_eulerian.beta_swap]
beta_set_is_alt_eq [lemma, in mathcomp_eulerian.beta_swap]
beta_compl [lemma, in mathcomp_eulerian.beta_swap]
beta_rev [lemma, in mathcomp_eulerian.beta]
beta_eulerian [lemma, in mathcomp_eulerian.beta]
beta_full [lemma, in mathcomp_eulerian.beta]
beta_swap_lt_caseA [lemma, in mathcomp_eulerian.perm_seq_bridge]
beta_swap [library]
beta_bridge [library]
beta_omega [library]
beta0 [lemma, in mathcomp_eulerian.beta]
binS' [lemma, in mathcomp_eulerian.eulerian]
block_chain_values [lemma, in mathcomp_eulerian.beta_omega]
block_chain_step [lemma, in mathcomp_eulerian.beta_omega]
block_right_maximal [lemma, in mathcomp_eulerian.beta_omega]
block_left_minimal [lemma, in mathcomp_eulerian.beta_omega]
block_left_le_right [lemma, in mathcomp_eulerian.beta_omega]
block_descent_chain [lemma, in mathcomp_eulerian.beta_omega]
block_right_descent [lemma, in mathcomp_eulerian.beta_omega]
block_left_descent [lemma, in mathcomp_eulerian.beta_omega]
block_right_ge [lemma, in mathcomp_eulerian.beta_omega]
block_left_le [lemma, in mathcomp_eulerian.beta_omega]
block_right_max [lemma, in mathcomp_eulerian.beta_omega]
block_left_min [lemma, in mathcomp_eulerian.beta_omega]
block_right_right_ok [lemma, in mathcomp_eulerian.beta_omega]
block_left_left_ok [lemma, in mathcomp_eulerian.beta_omega]
block_right [definition, in mathcomp_eulerian.beta_omega]
block_left [definition, in mathcomp_eulerian.beta_omega]
bool_triangle [lemma, in mathcomp_eulerian.altsub]
Bridges [section, in mathcomp_eulerian.psi_descent_v2]
Bridges.Hmm [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.s [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.sl [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.sr [variable, in mathcomp_eulerian.psi_descent_v2]
Bridges.x [variable, in mathcomp_eulerian.psi_descent_v2]

C

Cancellation [section, in mathcomp_eulerian.perm_compress]
Cancellation.n [variable, in mathcomp_eulerian.perm_compress]
card_split_ord_pair [lemma, in mathcomp_eulerian.inversions]
card_ord_pair [lemma, in mathcomp_eulerian.inversions]
card_turn_witness [lemma, in mathcomp_eulerian.altsub]
card_turn_image [lemma, in mathcomp_eulerian.altsub]
card_turn_iv_le [lemma, in mathcomp_eulerian.altsub]
card_slot_iv [lemma, in mathcomp_eulerian.altsub]
card_eq_ord_max_fiber [lemma, in mathcomp_eulerian.stirling_fiber]
card_neq_ord_max_fiber [lemma, in mathcomp_eulerian.stirling_fiber]
cde [inductive, in mathcomp_eulerian.psi_cdindex_defs]
cde_total_width_phi_w [lemma, in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_phi_w_all [lemma, in mathcomp_eulerian.psi_cdindex_support]
cde_sind [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_rec [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_ind [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_rect [definition, in mathcomp_eulerian.psi_cdindex_defs]
cde_total_width_cat [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_D_succ [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_C_succ [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_total_width [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
cde_width [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono_apply_psis_D_bit_self [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_D_bit_pred [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_C_bit [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_psi_effect [lemma, in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_inj [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono_apply_psis_mem [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono_self_mem [lemma, in mathcomp_eulerian.psi_cdindex_support]
char_mono [definition, in mathcomp_eulerian.psi_cdindex_defs]
char_mono_in_expand_cde [lemma, in mathcomp_eulerian.perm_seq_bridge]
char_mono_class_inj [lemma, in mathcomp_eulerian.perm_seq_bridge]
char_mono_perm_to_seq [lemma, in mathcomp_eulerian.perm_seq_bridge]
check_fact3_size1 [lemma, in mathcomp_eulerian.psi_cdindex_core]
check_fact3P [lemma, in mathcomp_eulerian.psi_cdindex_core]
check_fact3 [definition, in mathcomp_eulerian.psi_cdindex_core]
check_fact3_true [lemma, in mathcomp_eulerian.psi_cdindex_support]
check_fact3_of_perm_eq [lemma, in mathcomp_eulerian.psi_cdindex_support]
check_strict_witness_correct [lemma, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_sw_3_0 [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_strict_witness [definition, in mathcomp_eulerian.psi_cdindex_witness]
check_phi_w_support [definition, in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_right [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_left [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde_psi [lemma, in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde [definition, in mathcomp_eulerian.psi_cdindex_defs]
classify_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
classify_skip_mm0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
class_map [definition, in mathcomp_eulerian.perm_seq_bridge]
class_char_monos_uniq [lemma, in mathcomp_eulerian.perm_seq_bridge]
cmp_out_of_range_left [lemma, in mathcomp_eulerian.psi_descent_thms]
cmp_out_of_range [lemma, in mathcomp_eulerian.psi_descent_thms]
coinv_set [definition, in mathcomp_eulerian.inversions]
compl_perm_involutive [lemma, in mathcomp_eulerian.beta_swap]
compl_perm_inj [lemma, in mathcomp_eulerian.beta_swap]
compl_permE [lemma, in mathcomp_eulerian.beta_swap]
compl_perm [definition, in mathcomp_eulerian.beta_swap]
constant_descent_monotone [lemma, in mathcomp_eulerian.altsub]
count_lt_cat [lemma, in mathcomp_eulerian.foata]
count_lt_perm_eq [lemma, in mathcomp_eulerian.foata]
count_lt [definition, in mathcomp_eulerian.foata]
count_gt_cat [lemma, in mathcomp_eulerian.foata]
count_gt_cons [lemma, in mathcomp_eulerian.foata]
count_gt_perm_eq [lemma, in mathcomp_eulerian.foata]
count_gt [definition, in mathcomp_eulerian.foata]
cross_inv_perm_eq_l [lemma, in mathcomp_eulerian.foata]
cross_inv_perm_eq_r [lemma, in mathcomp_eulerian.foata]
cross_inv_cat_r [lemma, in mathcomp_eulerian.foata]
cross_inv_cat_l [lemma, in mathcomp_eulerian.foata]
cross_inv_cons [lemma, in mathcomp_eulerian.foata]
cross_inv_rcons [lemma, in mathcomp_eulerian.foata]
cross_inv_nil_l [lemma, in mathcomp_eulerian.foata]
cross_inv_nil_r [lemma, in mathcomp_eulerian.foata]
cross_inv [definition, in mathcomp_eulerian.foata]
CycleBasic [section, in mathcomp_eulerian.cycles]
CycleCountInsertAfter [section, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.j0 [variable, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.n [variable, in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.s [variable, in mathcomp_eulerian.stirling_fiber]
cycles [library]
cycles_rec [library]
cycle_count_id [lemma, in mathcomp_eulerian.cycles]
cycle_count_le [lemma, in mathcomp_eulerian.cycles]
cycle_count [definition, in mathcomp_eulerian.cycles]
cycle_count_lift_perm_id [lemma, in mathcomp_eulerian.cycles_rec]
cycle_count_insert_after [lemma, in mathcomp_eulerian.stirling_fiber]
cyc_last_to_front_wf [lemma, in mathcomp_eulerian.foata]
cyc_last_to_frontK [lemma, in mathcomp_eulerian.foata]
cyc_first_to_backK [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back_uniq [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back_perm_eq [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back_size [lemma, in mathcomp_eulerian.foata]
cyc_first_to_back [definition, in mathcomp_eulerian.foata]
cyc_diff_block_gt [lemma, in mathcomp_eulerian.foata]
cyc_diff_block_lt [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_rcons [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_uniq [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_size [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front_perm_eq [lemma, in mathcomp_eulerian.foata]
cyc_last_to_front [definition, in mathcomp_eulerian.foata]
C_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]

D

des [definition, in mathcomp_eulerian.descent]
Descent [section, in mathcomp_eulerian.descent]
descent [library]
DescentDrop [section, in mathcomp_eulerian.descent]
DescentDrop.n [variable, in mathcomp_eulerian.descent]
DescentReverse [section, in mathcomp_eulerian.descent]
DescentReverse.n [variable, in mathcomp_eulerian.descent]
descent_psi_effect [lemma, in mathcomp_eulerian.psi_cdindex_core]
descent_psi_LR_swap1_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add_ex [definition, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2 [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap1 [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_lboundary_R [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_rboundary [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_psi_interior [lemma, in mathcomp_eulerian.psi_descent_thms]
descent_set_compl [lemma, in mathcomp_eulerian.beta_swap]
descent_set [definition, in mathcomp_eulerian.descent]
descent_set_full_rev [lemma, in mathcomp_eulerian.beta]
descent_set_rev_perm_ord [lemma, in mathcomp_eulerian.beta]
descent_set_rev_perm [lemma, in mathcomp_eulerian.beta]
descent_to_bvec_inj [lemma, in mathcomp_eulerian.perm_seq_bridge]
descent_to_bvec [definition, in mathcomp_eulerian.perm_seq_bridge]
Descent.n [variable, in mathcomp_eulerian.descent]
desc_positions_bvec [lemma, in mathcomp_eulerian.perm_seq_bridge]
DesInsertMax [section, in mathcomp_eulerian.eulerian]
DesInsertMax.n [variable, in mathcomp_eulerian.eulerian]
DesInsertMax.t [variable, in mathcomp_eulerian.eulerian]
des_insert_max_interior [lemma, in mathcomp_eulerian.eulerian]
des_insert_max_ord_max [lemma, in mathcomp_eulerian.eulerian]
des_insert_max_ord0 [lemma, in mathcomp_eulerian.eulerian]
des_rev_perm_ord [lemma, in mathcomp_eulerian.descent]
des_rev_perm [lemma, in mathcomp_eulerian.descent]
des_id [lemma, in mathcomp_eulerian.descent]
des_add_asc [lemma, in mathcomp_eulerian.descent]
des_le [lemma, in mathcomp_eulerian.descent]
des0_id [lemma, in mathcomp_eulerian.eulerian]
dir_right_of_turn [lemma, in mathcomp_eulerian.altsub]
dir_left_of_turn [lemma, in mathcomp_eulerian.altsub]
DropPerm [section, in mathcomp_eulerian.perm_compress]
DropPerm.n [variable, in mathcomp_eulerian.perm_compress]
DropPerm.s [variable, in mathcomp_eulerian.perm_compress]
drop_psi_above [lemma, in mathcomp_eulerian.psi_core]
drop_mm_psi [lemma, in mathcomp_eulerian.psi_core]
drop_psi [lemma, in mathcomp_eulerian.psi_core]
drop_perm_lift_perm [lemma, in mathcomp_eulerian.perm_compress]
drop_permE [lemma, in mathcomp_eulerian.perm_compress]
drop_perm [definition, in mathcomp_eulerian.perm_compress]
drop_fun_inj [lemma, in mathcomp_eulerian.perm_compress]
drop_funE [lemma, in mathcomp_eulerian.perm_compress]
drop_fun [definition, in mathcomp_eulerian.perm_compress]
drop_fun_ne [lemma, in mathcomp_eulerian.perm_compress]
drop_mm_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
drop1_witness_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
D_vertex_descent_transition [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_phi_w_eq_S_w_seq [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cat_D [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cons_C [lemma, in mathcomp_eulerian.psi_cdindex_support]
D_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]
D_offsets [definition, in mathcomp_eulerian.psi_cdindex_support_defs]

E

elem_rs_in_range [lemma, in mathcomp_eulerian.psi_descent_thms]
elem_in_range [lemma, in mathcomp_eulerian.psi_descent_thms]
endpoint_succ_is_D_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
endpoint_next_has_left_child_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_next_has_left_child_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_has_left_child [lemma, in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_t [lemma, in mathcomp_eulerian.psi_cdindex_tree]
enum_ord_split [lemma, in mathcomp_eulerian.altsub]
Equidistribution [section, in mathcomp_eulerian.foata]
Equidistribution.FoataPerm [section, in mathcomp_eulerian.foata]
Equidistribution.FoataPerm.n [variable, in mathcomp_eulerian.foata]
eulerian [definition, in mathcomp_eulerian.eulerian]
eulerian [library]
EulerianBasic [section, in mathcomp_eulerian.eulerian]
eulerian_explicit [lemma, in mathcomp_eulerian.eulerian]
eulerian_rec [lemma, in mathcomp_eulerian.eulerian]
eulerian_n_n [lemma, in mathcomp_eulerian.eulerian]
eulerian_symm [lemma, in mathcomp_eulerian.eulerian]
eulerian_n_0 [lemma, in mathcomp_eulerian.eulerian]
eulerian_out_of_range [lemma, in mathcomp_eulerian.eulerian]
eulerian_row_sum_fact [lemma, in mathcomp_eulerian.eulerian]
eulerian_row_sum [lemma, in mathcomp_eulerian.eulerian]
eul_pol [definition, in mathcomp_eulerian.qeul]
exactly_one_descent_LR_ex [definition, in mathcomp_eulerian.psi_descent_v2]
exactly_one_descent_LR [lemma, in mathcomp_eulerian.psi_descent_v2]
ExistenceLB [section, in mathcomp_eulerian.altsub]
ExistenceLB.n [variable, in mathcomp_eulerian.altsub]
expand_cde [definition, in mathcomp_eulerian.psi_cdindex_defs]
expand_cde_mem_iff [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
expand_cde_mem_transitions [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
ExtractMax [section, in mathcomp_eulerian.eulerian]
ExtractMax.n [variable, in mathcomp_eulerian.eulerian]
ExtractMax.p [variable, in mathcomp_eulerian.eulerian]
ExtractMax.s [variable, in mathcomp_eulerian.eulerian]
ExtractMax.sp [variable, in mathcomp_eulerian.eulerian]
extract_insert_maxPI [lemma, in mathcomp_eulerian.eulerian]
extract_insert_max [lemma, in mathcomp_eulerian.eulerian]
extract_max_widen [lemma, in mathcomp_eulerian.eulerian]
extract_max_permE [lemma, in mathcomp_eulerian.eulerian]
extract_max_perm [definition, in mathcomp_eulerian.eulerian]
extract_max_fun_inj [lemma, in mathcomp_eulerian.eulerian]
extract_max_funE [lemma, in mathcomp_eulerian.eulerian]
extract_max_fun [definition, in mathcomp_eulerian.eulerian]
extract_max_ne [lemma, in mathcomp_eulerian.eulerian]
ex_roundtrip_compute [definition, in mathcomp_eulerian.mmtree]
ex_roundtrip [definition, in mathcomp_eulerian.mmtree]
ex_nontrivial [definition, in mathcomp_eulerian.mmtree]
ex_seq [definition, in mathcomp_eulerian.mmtree]
E_letter [constructor, in mathcomp_eulerian.psi_cdindex_defs]

F

fact3 [lemma, in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_213 [definition, in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_315426 [definition, in mathcomp_eulerian.psi_cdindex_support]
find_ss_spec [lemma, in mathcomp_eulerian.perm_seq_bridge]
find_ss [definition, in mathcomp_eulerian.perm_seq_bridge]
flip_count_perm_seq_eq_turn_count [lemma, in mathcomp_eulerian.altsub]
flip_count_as_sum [lemma, in mathcomp_eulerian.altsub]
flip_count_pick_le_perm [lemma, in mathcomp_eulerian.altsub]
flip_count_is_alt_bool [lemma, in mathcomp_eulerian.altsub]
flip_count_sign_seq_le_subseq [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_le_subseq [lemma, in mathcomp_eulerian.altsub]
flip_count_sign_seq_insert_front [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_insert_anywhere [lemma, in mathcomp_eulerian.altsub]
flip_step_helper [lemma, in mathcomp_eulerian.altsub]
flip_count_pairmap_insert [lemma, in mathcomp_eulerian.altsub]
flip_count_cons2 [lemma, in mathcomp_eulerian.altsub]
flip_count [definition, in mathcomp_eulerian.altsub]
foata [definition, in mathcomp_eulerian.foata]
foata [library]
FoataBlocks [section, in mathcomp_eulerian.beta_omega]
FoataBlocks.n [variable, in mathcomp_eulerian.beta_omega]
foata_perm_inj [lemma, in mathcomp_eulerian.foata]
foata_perm_inv_maj [lemma, in mathcomp_eulerian.foata]
foata_perm [definition, in mathcomp_eulerian.foata]
foata_perm_to_seq_bnd [lemma, in mathcomp_eulerian.foata]
foata_perm_to_seq_uniq [lemma, in mathcomp_eulerian.foata]
foata_perm_to_seq_size [lemma, in mathcomp_eulerian.foata]
foata_inj_uniq [lemma, in mathcomp_eulerian.foata]
foata_invK [lemma, in mathcomp_eulerian.foata]
foata_invK_aux [lemma, in mathcomp_eulerian.foata]
foata_inv [definition, in mathcomp_eulerian.foata]
foata_inv_aux [definition, in mathcomp_eulerian.foata]
foata_step_undoK [lemma, in mathcomp_eulerian.foata]
foata_step_undo [definition, in mathcomp_eulerian.foata]
foata_inv_eq_maj [lemma, in mathcomp_eulerian.foata]
foata_step_inv [lemma, in mathcomp_eulerian.foata]
foata_step_inv_gt [lemma, in mathcomp_eulerian.foata]
foata_step_inv_lt [lemma, in mathcomp_eulerian.foata]
foata_last_eq [lemma, in mathcomp_eulerian.foata]
foata_last [lemma, in mathcomp_eulerian.foata]
foata_rcons [lemma, in mathcomp_eulerian.foata]
foata_step_last [lemma, in mathcomp_eulerian.foata]
foata_all_lt [lemma, in mathcomp_eulerian.foata]
foata_uniq [lemma, in mathcomp_eulerian.foata]
foata_size [lemma, in mathcomp_eulerian.foata]
foata_perm_eq [lemma, in mathcomp_eulerian.foata]
foata_step_uniq [lemma, in mathcomp_eulerian.foata]
foata_step_size [lemma, in mathcomp_eulerian.foata]
foata_step_perm_eq [lemma, in mathcomp_eulerian.foata]
foata_step [definition, in mathcomp_eulerian.foata]
foldr_maxn_set_to_seq_lb [lemma, in mathcomp_eulerian.beta_bridge]
foldr_maxn_ge [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
foldr_maxn_ge_nth [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_le_nth [lemma, in mathcomp_eulerian.psi_core]
foldr_maxn_ge [lemma, in mathcomp_eulerian.psi_core]
foldr_maxn_aux [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_le [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_aux [lemma, in mathcomp_eulerian.psi_core]
foldr_minn_all_gt' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_minn_ge' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_path' [lemma, in mathcomp_eulerian.psi_cdindex_witness]

G

geq_minn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
geq_maxn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]

H

has_left_child_is_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last_fuel [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_t_last_valid [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
has_left_child_psi [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_order_iso [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_of_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
has_transition_omega_seq [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons2 [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition [definition, in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_0 [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_gt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_lt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_psi_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_iota [lemma, in mathcomp_eulerian.psi_cdindex_witness]
has_left_child_true [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_false [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_cons [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_monotone [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_0 [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_0 [lemma, in mathcomp_eulerian.psi_descent_v2]
has_left_child [definition, in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel [definition, in mathcomp_eulerian.psi_descent_v2]
head_max_is_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
head_min_not_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
head_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
hlc_core_1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
hlc_core_not1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
hlc_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]
H1 [section, in mathcomp_eulerian.cycles_rec]
H1.n [variable, in mathcomp_eulerian.cycles_rec]
H1.s [variable, in mathcomp_eulerian.cycles_rec]

I

imset_rev_ord_compl [lemma, in mathcomp_eulerian.beta]
imset_rev_ord_inv [lemma, in mathcomp_eulerian.beta]
index_rcons_eq_size [lemma, in mathcomp_eulerian.psi_cdindex_core]
index_map_inj_in [lemma, in mathcomp_eulerian.psi_comm]
index_lt_sorted [lemma, in mathcomp_eulerian.perm_seq_bridge]
InsertAfter [section, in mathcomp_eulerian.stirling_fiber]
InsertAfter.n [variable, in mathcomp_eulerian.stirling_fiber]
InsertExtractBij [section, in mathcomp_eulerian.eulerian]
InsertExtractBij.n [variable, in mathcomp_eulerian.eulerian]
InsertMax [section, in mathcomp_eulerian.eulerian]
InsertMax.n [variable, in mathcomp_eulerian.eulerian]
InsertMax.p [variable, in mathcomp_eulerian.eulerian]
InsertMax.t [variable, in mathcomp_eulerian.eulerian]
insert_max_perm_bij [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_pair_surj [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_pair_inj [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_fiber [lemma, in mathcomp_eulerian.eulerian]
insert_extract_max [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_lift [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm_at_p [lemma, in mathcomp_eulerian.eulerian]
insert_max_permE [lemma, in mathcomp_eulerian.eulerian]
insert_max_perm [definition, in mathcomp_eulerian.eulerian]
insert_max_fun_inj [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun_lift [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun_p [lemma, in mathcomp_eulerian.eulerian]
insert_max_fun [definition, in mathcomp_eulerian.eulerian]
insert_after_surj [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_inj_pair [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_decomp [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max_neq [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_other [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_j0 [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max [lemma, in mathcomp_eulerian.stirling_fiber]
insert_afterE [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after [definition, in mathcomp_eulerian.stirling_fiber]
insert_after_fun_inj [lemma, in mathcomp_eulerian.stirling_fiber]
insert_after_fun [definition, in mathcomp_eulerian.stirling_fiber]
interior_val_bounds [lemma, in mathcomp_eulerian.altsub]
interior_is_turn_inj [lemma, in mathcomp_eulerian.altsub]
internal_vertices_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
internal_vertices [definition, in mathcomp_eulerian.psi_cdindex_defs]
InterTurn [section, in mathcomp_eulerian.altsub]
InterTurn.n [variable, in mathcomp_eulerian.altsub]
inter_turn_monotone_strict [lemma, in mathcomp_eulerian.altsub]
inter_turn_monotone [lemma, in mathcomp_eulerian.altsub]
inv [definition, in mathcomp_eulerian.inversions]
Inversions [section, in mathcomp_eulerian.inversions]
inversions [library]
Inversions.n [variable, in mathcomp_eulerian.inversions]
InvInsertMax [section, in mathcomp_eulerian.qfact]
InvInsertMax.n [variable, in mathcomp_eulerian.qfact]
InvInsertMax.p [variable, in mathcomp_eulerian.qfact]
InvInsertMax.t [variable, in mathcomp_eulerian.qfact]
InvMajBoundsRev [section, in mathcomp_eulerian.inversions]
InvMajBoundsRev.n [variable, in mathcomp_eulerian.inversions]
inv_rev_perm [lemma, in mathcomp_eulerian.inversions]
inv_rev_perm_eq_coinv [lemma, in mathcomp_eulerian.inversions]
inv_le [lemma, in mathcomp_eulerian.inversions]
inv_double_sum [lemma, in mathcomp_eulerian.inversions]
inv_id [lemma, in mathcomp_eulerian.inversions]
inv_set [definition, in mathcomp_eulerian.inversions]
inv_q_fact [lemma, in mathcomp_eulerian.qfact]
inv_insert_max [lemma, in mathcomp_eulerian.qfact]
inv_via_sum [lemma, in mathcomp_eulerian.qfact]
inv_maj_equidistr [lemma, in mathcomp_eulerian.foata]
inv_eq_inv_seq [lemma, in mathcomp_eulerian.foata]
inv_seq_cons_eq_rcons_shift [lemma, in mathcomp_eulerian.foata]
inv_seq_flatten_swap_eq [lemma, in mathcomp_eulerian.foata]
inv_seq_cat [lemma, in mathcomp_eulerian.foata]
inv_seq_rcons [lemma, in mathcomp_eulerian.foata]
inv_seq [definition, in mathcomp_eulerian.foata]
in_internal_vertices [lemma, in mathcomp_eulerian.psi_cdindex_support]
iota_mem_range [lemma, in mathcomp_eulerian.psi_cdindex_witness]
is_internal_lt [lemma, in mathcomp_eulerian.psi_cdindex_core]
is_internal_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
is_inv [definition, in mathcomp_eulerian.inversions]
is_internal [definition, in mathcomp_eulerian.psi_cdindex_defs]
is_inv_lift_p [lemma, in mathcomp_eulerian.qfact]
is_inv_p_lift [lemma, in mathcomp_eulerian.qfact]
is_inv_lift_pair [lemma, in mathcomp_eulerian.qfact]
is_descent_compl [lemma, in mathcomp_eulerian.beta_swap]
is_desc_seq [definition, in mathcomp_eulerian.foata]
is_descent_rev [lemma, in mathcomp_eulerian.descent]
is_descent_drop [lemma, in mathcomp_eulerian.descent]
is_descentE [lemma, in mathcomp_eulerian.descent]
is_descent [definition, in mathcomp_eulerian.descent]
is_alt_pick_turn_witness [lemma, in mathcomp_eulerian.altsub]
is_alt_from_sign [lemma, in mathcomp_eulerian.altsub]
is_alt_flip_count [lemma, in mathcomp_eulerian.altsub]
is_alt_bool [definition, in mathcomp_eulerian.altsub]
is_alt_bool_aux [definition, in mathcomp_eulerian.altsub]
is_alt_subseq_strictmono_le2 [lemma, in mathcomp_eulerian.altsub]
is_alt_three [lemma, in mathcomp_eulerian.altsub]
is_alt_size_le1 [lemma, in mathcomp_eulerian.altsub]
is_alt_pick_seq_le2 [lemma, in mathcomp_eulerian.altsub]
is_alt_tail [lemma, in mathcomp_eulerian.altsub]
is_alt_cons2 [lemma, in mathcomp_eulerian.altsub]
is_alt_singleton [lemma, in mathcomp_eulerian.altsub]
is_alt_nil [lemma, in mathcomp_eulerian.altsub]
is_alt [definition, in mathcomp_eulerian.altsub]
is_turnE [lemma, in mathcomp_eulerian.altsub]
is_turn [definition, in mathcomp_eulerian.altsub]
is_descent_perm_seq [lemma, in mathcomp_eulerian.perm_seq_bridge]
is_internal_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
is_internal_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
is_D_letter [definition, in mathcomp_eulerian.psi_cdindex_witness]
is_descent_seq_ex [definition, in mathcomp_eulerian.psi_descent_v2]
is_descent_seq [definition, in mathcomp_eulerian.psi_descent_v2]

L

last_vertex_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
last_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
Leaf [constructor, in mathcomp_eulerian.mmtree]
left_ok_self [lemma, in mathcomp_eulerian.beta_omega]
left_ok [definition, in mathcomp_eulerian.beta_omega]
leq_seqb_anti [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_trans [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_total [lemma, in mathcomp_eulerian.psi_cdindex_core]
leq_seqb [definition, in mathcomp_eulerian.psi_cdindex_defs]
leq_lift [lemma, in mathcomp_eulerian.ordinal_reindex]
leq_maxn' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
LiftOrd [section, in mathcomp_eulerian.ordinal_reindex]
LiftOrd.n [variable, in mathcomp_eulerian.ordinal_reindex]
LiftPerm [section, in mathcomp_eulerian.perm_compress]
LiftPerm.k [variable, in mathcomp_eulerian.perm_compress]
LiftPerm.n [variable, in mathcomp_eulerian.perm_compress]
LiftPerm.t [variable, in mathcomp_eulerian.perm_compress]
lift_image [lemma, in mathcomp_eulerian.ordinal_reindex]
lift_perm_id_iter_lift [lemma, in mathcomp_eulerian.cycles_rec]
lift_perm_id_iter [lemma, in mathcomp_eulerian.cycles_rec]
lift_perm_ord_max_eq [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_drop_perm [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_ne_k [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_lift [lemma, in mathcomp_eulerian.perm_compress]
lift_perm_ord_max [lemma, in mathcomp_eulerian.perm_compress]
lift_permE [lemma, in mathcomp_eulerian.perm_compress]
lift_perm [definition, in mathcomp_eulerian.perm_compress]
lift_fun_inj [lemma, in mathcomp_eulerian.perm_compress]
lift_fun_lift [lemma, in mathcomp_eulerian.perm_compress]
lift_fun_ord_max [lemma, in mathcomp_eulerian.perm_compress]
lift_fun [definition, in mathcomp_eulerian.perm_compress]
lift_drop_permE [lemma, in mathcomp_eulerian.perm_compress]
LowerBound [section, in mathcomp_eulerian.altsub]
LowerBound.n [variable, in mathcomp_eulerian.altsub]
LR_pred_is_endpoint_ex3 [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex [definition, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint [lemma, in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_t [lemma, in mathcomp_eulerian.psi_cdindex_tree]
ltn_unlift_some [lemma, in mathcomp_eulerian.ordinal_reindex]
ltn_lift [lemma, in mathcomp_eulerian.ordinal_reindex]

M

maj [definition, in mathcomp_eulerian.inversions]
MajorIndex [section, in mathcomp_eulerian.inversions]
MajorIndex.n [variable, in mathcomp_eulerian.inversions]
maj_rev_perm [lemma, in mathcomp_eulerian.inversions]
maj_le [lemma, in mathcomp_eulerian.inversions]
maj_id [lemma, in mathcomp_eulerian.inversions]
maj_q_fact [lemma, in mathcomp_eulerian.qfact]
maj_eq_maj_seq [lemma, in mathcomp_eulerian.foata]
maj_seq_rcons [lemma, in mathcomp_eulerian.foata]
maj_seq [definition, in mathcomp_eulerian.foata]
map_mod_iota_rot [lemma, in mathcomp_eulerian.psi_core]
map_nth_iota_sorted [lemma, in mathcomp_eulerian.psi_core]
map_succ_order_iso [lemma, in mathcomp_eulerian.psi_cdindex_witness]
MaxAlternation [section, in mathcomp_eulerian.altsub]
MaxAlternation.n [variable, in mathcomp_eulerian.altsub]
max_eq_nth_sort_last [lemma, in mathcomp_eulerian.psi_core]
max_val_drop [lemma, in mathcomp_eulerian.psi_core]
max_val_perm_eq [lemma, in mathcomp_eulerian.psi_core]
max_pos_lt [lemma, in mathcomp_eulerian.psi_core]
max_in [lemma, in mathcomp_eulerian.psi_core]
max_pos [definition, in mathcomp_eulerian.psi_core]
max_pos_core_gt0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
max_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mem_inv_set [lemma, in mathcomp_eulerian.inversions]
mem_omega_set [lemma, in mathcomp_eulerian.beta_omega]
mem_set_to_seq_ord [lemma, in mathcomp_eulerian.beta_bridge]
mem_set_to_seq_iff [lemma, in mathcomp_eulerian.beta_bridge]
mem_set_to_seq [lemma, in mathcomp_eulerian.beta_bridge]
mem_alt_desc_set [lemma, in mathcomp_eulerian.beta_swap]
mem_descent_set [lemma, in mathcomp_eulerian.descent]
mem_pos_seq [lemma, in mathcomp_eulerian.altsub]
mem_turn_iv [lemma, in mathcomp_eulerian.altsub]
mem_slot_iv [lemma, in mathcomp_eulerian.altsub]
mem_omega_seq [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
mem_filter_iota_nth [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
min_pos_lt [lemma, in mathcomp_eulerian.mmtree]
min_in [lemma, in mathcomp_eulerian.mmtree]
min_pos [definition, in mathcomp_eulerian.mmtree]
min_eq_nth_sort_0 [lemma, in mathcomp_eulerian.psi_core]
min_val_drop [lemma, in mathcomp_eulerian.psi_core]
min_val_perm_eq [lemma, in mathcomp_eulerian.psi_core]
min_pos_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
min_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mmtree [inductive, in mathcomp_eulerian.mmtree]
MMTree [section, in mathcomp_eulerian.mmtree]
mmtree [library]
mmtree_shape_psi [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_decompose [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_order_iso [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_cons [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_nil [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel_monotone [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape [definition, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel [definition, in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seqK [lemma, in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel_correct [lemma, in mathcomp_eulerian.mmtree]
mmtree_of_seq [definition, in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel [definition, in mathcomp_eulerian.mmtree]
mmtree_to_seq [definition, in mathcomp_eulerian.mmtree]
mmtree_sind [definition, in mathcomp_eulerian.mmtree]
mmtree_rec [definition, in mathcomp_eulerian.mmtree]
mmtree_ind [definition, in mathcomp_eulerian.mmtree]
mmtree_rect [definition, in mathcomp_eulerian.mmtree]
mmtree_of_seq_mmK [lemma, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel_correct [lemma, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm [definition, in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel [definition, in mathcomp_eulerian.psi_core]
mm_pos_rcons_lt [lemma, in mathcomp_eulerian.psi_cdindex_core]
mm_pos_lt_pred [lemma, in mathcomp_eulerian.psi_cdindex_support]
mm_pos_drop_mm [lemma, in mathcomp_eulerian.psi_core]
mm_pos_order_iso [lemma, in mathcomp_eulerian.psi_core]
mm_pos_psi_eq [lemma, in mathcomp_eulerian.psi_core]
mm_pos_char [lemma, in mathcomp_eulerian.psi_core]
mm_pos_lt [lemma, in mathcomp_eulerian.psi_core]
mm_pos [definition, in mathcomp_eulerian.psi_core]
mm_pos_witness [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_min_first [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
mono_inj_in [lemma, in mathcomp_eulerian.psi_comm]

N

neg_add_neg [lemma, in mathcomp_eulerian.altsub]
nil_in_powerset_internal [lemma, in mathcomp_eulerian.perm_seq_bridge]
Node [constructor, in mathcomp_eulerian.mmtree]
notin_take_mm [lemma, in mathcomp_eulerian.psi_core]
not_set_is_alt_omega_not_full [lemma, in mathcomp_eulerian.beta_swap]
not_set_is_alt_n_ge2 [lemma, in mathcomp_eulerian.beta_swap]
not_is_descentE [lemma, in mathcomp_eulerian.altsub]
no_inner_in_pos_seq [lemma, in mathcomp_eulerian.altsub]
nth_char_mono [lemma, in mathcomp_eulerian.psi_cdindex_core]
nth_window_at [lemma, in mathcomp_eulerian.psi_descent_thms]
nth_w_mm_pos [lemma, in mathcomp_eulerian.psi_core]
nth_psi_inside [lemma, in mathcomp_eulerian.psi_core]
nth_psi_right [lemma, in mathcomp_eulerian.psi_core]
nth_psi_left [lemma, in mathcomp_eulerian.psi_core]
nth_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
nth_descent_to_bvec [lemma, in mathcomp_eulerian.perm_seq_bridge]
nth_perm_to_seq [lemma, in mathcomp_eulerian.perm_seq_bridge]

O

omega_set [definition, in mathcomp_eulerian.beta_omega]
omega_set_seq_local_bridge [lemma, in mathcomp_eulerian.beta_bridge]
omega_seq_local [definition, in mathcomp_eulerian.beta_bridge]
omega_set_alt_full [lemma, in mathcomp_eulerian.beta_swap]
omega_proper_beta_lt [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_seq_subset_bounded [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_set_seq_bridge_bounded [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_seq_mem_eq [lemma, in mathcomp_eulerian.perm_seq_bridge]
omega_monotone_class_count [lemma, in mathcomp_eulerian.psi_cdindex_witness]
omega_seq [definition, in mathcomp_eulerian.psi_cdindex_witness]
order_iso_drop [lemma, in mathcomp_eulerian.psi_core]
order_iso_take [lemma, in mathcomp_eulerian.psi_core]
ordinal_reindex [library]
ord_max_notin_turn_image [lemma, in mathcomp_eulerian.altsub]
ord0_neq_ord_max [lemma, in mathcomp_eulerian.altsub]
ord0_notin_turn_image [lemma, in mathcomp_eulerian.altsub]

P

path_iota' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
path_leq_last' [lemma, in mathcomp_eulerian.psi_cdindex_witness]
perm_eq_from_subset [lemma, in mathcomp_eulerian.psi_cdindex_support]
perm_eq_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
perm_to_seq_foata_perm [lemma, in mathcomp_eulerian.foata]
perm_eq_flatten_map_pred [lemma, in mathcomp_eulerian.foata]
perm_eq_flatten_map_cyc [lemma, in mathcomp_eulerian.foata]
perm_seq [definition, in mathcomp_eulerian.altsub]
perm_to_seq_class_map [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_seq_to_perm [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_bnd [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_inj [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_uniq [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_size [lemma, in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq [definition, in mathcomp_eulerian.perm_seq_bridge]
perm_seq_bridge [library]
perm_compress [library]
phi_w_as_map [lemma, in mathcomp_eulerian.psi_cdindex_core]
phi_w_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
phi_w_support_general [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w_decomp_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w_cons_mm0 [lemma, in mathcomp_eulerian.psi_cdindex_support]
phi_w [definition, in mathcomp_eulerian.psi_cdindex_defs]
phi_w_support_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
phi'_w [definition, in mathcomp_eulerian.psi_cdindex_defs]
PickSeqFull [section, in mathcomp_eulerian.altsub]
PickSeqFull.n [variable, in mathcomp_eulerian.altsub]
pick_seq_subseq_perm_seq [lemma, in mathcomp_eulerian.altsub]
pick_seq_pos_seq [lemma, in mathcomp_eulerian.altsub]
pick_flip_has_turn [lemma, in mathcomp_eulerian.altsub]
pick_seq_setT [lemma, in mathcomp_eulerian.altsub]
pick_seq [definition, in mathcomp_eulerian.altsub]
porbits_lift_perm_id [lemma, in mathcomp_eulerian.cycles_rec]
porbit_id_singleton [lemma, in mathcomp_eulerian.cycles]
porbit_lift_perm_id_lift [lemma, in mathcomp_eulerian.cycles_rec]
porbit_lift_perm_id_max [lemma, in mathcomp_eulerian.cycles_rec]
post_window_extremum_ex [definition, in mathcomp_eulerian.psi_descent_v2]
post_window_extremum [lemma, in mathcomp_eulerian.psi_descent_v2]
pos_seq_last_val [lemma, in mathcomp_eulerian.altsub]
pos_seq_nth0 [lemma, in mathcomp_eulerian.altsub]
pos_seq_val_lt_inv [lemma, in mathcomp_eulerian.altsub]
pos_seq_val_lt [lemma, in mathcomp_eulerian.altsub]
pos_seq_strict_sorted [lemma, in mathcomp_eulerian.altsub]
pos_seq_uniq [lemma, in mathcomp_eulerian.altsub]
pos_seq [definition, in mathcomp_eulerian.altsub]
powerset_internal [definition, in mathcomp_eulerian.psi_cdindex_defs]
powerset_internal_apply_psis [lemma, in mathcomp_eulerian.perm_seq_bridge]
pred_sub_add [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_extremum_R [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_ex [definition, in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_when_max_head [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_window_lt_max_when_min_head [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_win_gt_min_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
pre_win_lt_max_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
psi [definition, in mathcomp_eulerian.psi_core]
psi_comm_nontrivial [definition, in mathcomp_eulerian.psi_comm]
psi_comm_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_nested_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm_nested [lemma, in mathcomp_eulerian.psi_comm]
psi_map_comm [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_ex [definition, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint [lemma, in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_lr [lemma, in mathcomp_eulerian.psi_comm]
psi_0_eq [lemma, in mathcomp_eulerian.psi_core]
psi_involutive [lemma, in mathcomp_eulerian.psi_core]
psi_id_trivial [lemma, in mathcomp_eulerian.psi_core]
psi_id_oor [lemma, in mathcomp_eulerian.psi_core]
psi_involutive_ex [definition, in mathcomp_eulerian.psi_core]
psi_nontrivial [definition, in mathcomp_eulerian.psi_core]
psi_perm_eq [lemma, in mathcomp_eulerian.psi_core]
psi_apply_psis_comm [lemma, in mathcomp_eulerian.perm_seq_bridge]
psi_descent_v2 [library]
psi_cdindex_support [library]
psi_comm [library]
psi_cdindex_tree_shape [library]
psi_cdindex_tree_hlc [library]
psi_cdindex_tree [library]
psi_cdindex_defs [library]
psi_descent [library]
psi_core [library]
psi_descent_thms [library]
psi_cdindex_witness [library]
psi_cdindex_core [library]
psi_cdindex_support_defs [library]

Q

qeul [library]
qfact [library]
qpow [abbreviation, in mathcomp_eulerian.qeul]
q_fact [definition, in mathcomp_eulerian.qfact]
q_int [definition, in mathcomp_eulerian.qfact]
q_eul_pol_q1 [lemma, in mathcomp_eulerian.qeul]
q_eul_pol_t1 [lemma, in mathcomp_eulerian.qeul]
q_eul_pol [definition, in mathcomp_eulerian.qeul]
q1_subst [definition, in mathcomp_eulerian.qeul]

R

rank_shift_psi_comm [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_map_comm [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_preserves_interior_order [lemma, in mathcomp_eulerian.psi_comm]
rank_shift_head_max_to_min [lemma, in mathcomp_eulerian.psi_core]
rank_shift_head_min_to_max [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seq_involutive [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seqE [lemma, in mathcomp_eulerian.psi_core]
rank_shift_perm_eq [lemma, in mathcomp_eulerian.psi_core]
rank_shift_seq [definition, in mathcomp_eulerian.psi_core]
rank_shift_interior_order_ex [definition, in mathcomp_eulerian.psi_descent_v2]
rev_ord_lt [lemma, in mathcomp_eulerian.inversions]
rev_perm_involutive [lemma, in mathcomp_eulerian.eulerian]
rev_perm_inj [lemma, in mathcomp_eulerian.eulerian]
rev_permE [lemma, in mathcomp_eulerian.descent]
rev_perm [definition, in mathcomp_eulerian.descent]
rev_perm_ordE [lemma, in mathcomp_eulerian.descent]
rev_perm_ord [definition, in mathcomp_eulerian.descent]
right_ok_self [lemma, in mathcomp_eulerian.beta_omega]
right_ok [definition, in mathcomp_eulerian.beta_omega]
rs_head_min_no_descent [lemma, in mathcomp_eulerian.psi_descent_thms]
rs_head_max_descent [lemma, in mathcomp_eulerian.psi_descent_thms]

S

sanity_inv_eq_maj3 [lemma, in mathcomp_eulerian.foata]
sanity_inv_eq_maj2 [lemma, in mathcomp_eulerian.foata]
sanity_inv_eq_maj [lemma, in mathcomp_eulerian.foata]
sanity_insert_after_pointwise [lemma, in mathcomp_eulerian.stirling_fiber]
SeqToPerm [section, in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.Hbnd [variable, in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.Hsz [variable, in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.Huniq [variable, in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.n [variable, in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.w [variable, in mathcomp_eulerian.perm_seq_bridge]
seq_cat_right_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_cat_left_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_to_perm_perm_to_seq [lemma, in mathcomp_eulerian.perm_seq_bridge]
seq_to_perm_nth [lemma, in mathcomp_eulerian.perm_seq_bridge]
seq_to_perm [definition, in mathcomp_eulerian.perm_seq_bridge]
seq_to_fun_inj [lemma, in mathcomp_eulerian.perm_seq_bridge]
seq_to_fun [definition, in mathcomp_eulerian.perm_seq_bridge]
seq_nth_bound [lemma, in mathcomp_eulerian.perm_seq_bridge]
set_to_seq_bound [lemma, in mathcomp_eulerian.beta_bridge]
set_to_seq [definition, in mathcomp_eulerian.beta_bridge]
set_is_alt_classify [lemma, in mathcomp_eulerian.beta_swap]
set_not_altP [lemma, in mathcomp_eulerian.beta_swap]
set_is_alt [definition, in mathcomp_eulerian.beta_swap]
shift_preserves_ltn [lemma, in mathcomp_eulerian.psi_comm]
sigma [abbreviation, in mathcomp_eulerian.stirling_fiber]
SignPerm [section, in mathcomp_eulerian.altsub]
SignPerm.n [variable, in mathcomp_eulerian.altsub]
sign_seq_alt_of_triple_flip [lemma, in mathcomp_eulerian.altsub]
sign_pair_neq [lemma, in mathcomp_eulerian.altsub]
sign_flip_at_turn [lemma, in mathcomp_eulerian.altsub]
sign_seq_is_alt [lemma, in mathcomp_eulerian.altsub]
sign_seq_perm_seq [lemma, in mathcomp_eulerian.altsub]
sign_seq_cons2 [lemma, in mathcomp_eulerian.altsub]
sign_seq [definition, in mathcomp_eulerian.altsub]
size_expand_cde_phi_w [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_phi_w [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_char_mono [lemma, in mathcomp_eulerian.psi_cdindex_core]
size_window_at [lemma, in mathcomp_eulerian.psi_descent_thms]
size_mmtree_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
size_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
size_count_lt_gt [lemma, in mathcomp_eulerian.foata]
size_pos_seq [lemma, in mathcomp_eulerian.altsub]
size_take_drop_skip [lemma, in mathcomp_eulerian.altsub]
size_sign_seq_perm [lemma, in mathcomp_eulerian.altsub]
size_sign_seq [lemma, in mathcomp_eulerian.altsub]
size_perm_seq [lemma, in mathcomp_eulerian.altsub]
size_in_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
size_psi [lemma, in mathcomp_eulerian.psi_core]
size_rank_shift_seq2 [lemma, in mathcomp_eulerian.psi_core]
size_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
size_descent_to_bvec [lemma, in mathcomp_eulerian.perm_seq_bridge]
size_mmtree_to_seq_node [lemma, in mathcomp_eulerian.psi_cdindex_tree]
size_witness_perm [lemma, in mathcomp_eulerian.psi_cdindex_witness]
SlotInterval [section, in mathcomp_eulerian.altsub]
SlotInterval.n [variable, in mathcomp_eulerian.altsub]
slot_descent_const_strict [lemma, in mathcomp_eulerian.altsub]
slot_descent_const [lemma, in mathcomp_eulerian.altsub]
slot_iv [definition, in mathcomp_eulerian.altsub]
sorted_uniq_nth_ltn [lemma, in mathcomp_eulerian.psi_comm]
sorted_val_enum_ord [lemma, in mathcomp_eulerian.altsub]
sorted_last_ge [lemma, in mathcomp_eulerian.psi_core]
sorted_head_le [lemma, in mathcomp_eulerian.psi_core]
sort_perm_eq_leq_seqb [lemma, in mathcomp_eulerian.psi_cdindex_core]
sort_map_mono [lemma, in mathcomp_eulerian.psi_comm]
sort_enum_subseq_enum [lemma, in mathcomp_eulerian.altsub]
sort_enum_strict_sorted [lemma, in mathcomp_eulerian.altsub]
sort_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
split_blocks_inv_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_cyc_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_block_then_P [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_one_block [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_app_notP [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_cons_notP [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_cons_P [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks_inv_aux_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks_inv [definition, in mathcomp_eulerian.foata]
split_blocks_inv_aux [definition, in mathcomp_eulerian.foata]
split_blocks_gt_strict [lemma, in mathcomp_eulerian.foata]
split_blocks_lt_strict [lemma, in mathcomp_eulerian.foata]
split_blocks_size_eq [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_size_when_last_P [lemma, in mathcomp_eulerian.foata]
split_blocks_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_wf [lemma, in mathcomp_eulerian.foata]
split_blocks_all_nonempty [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_all_nonempty [lemma, in mathcomp_eulerian.foata]
split_blocks_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks_aux_flatten [lemma, in mathcomp_eulerian.foata]
split_blocks [definition, in mathcomp_eulerian.foata]
split_blocks_aux [definition, in mathcomp_eulerian.foata]
stirling_c_row_sum_fact [lemma, in mathcomp_eulerian.cycles]
stirling_c_row_sum [lemma, in mathcomp_eulerian.cycles]
stirling_c [definition, in mathcomp_eulerian.cycles]
stirling_c_rec [lemma, in mathcomp_eulerian.stirling_fiber]
stirling_fiber [library]
strict_witness_ex3 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_exists [lemma, in mathcomp_eulerian.psi_cdindex_witness]
subseq_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
subseq_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
subseq_drop_extra [lemma, in mathcomp_eulerian.altsub]
subset_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
subset_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
sum_succ_ord_eq_bin2 [lemma, in mathcomp_eulerian.inversions]
sum_ascent [lemma, in mathcomp_eulerian.eulerian]
sum_descent [lemma, in mathcomp_eulerian.eulerian]
sum_geq_p [lemma, in mathcomp_eulerian.qfact]
sum_rev_X [lemma, in mathcomp_eulerian.qfact]
sum_des_eq_eul_pol [lemma, in mathcomp_eulerian.qeul]
sum_inv_cyc_gt_blocks [lemma, in mathcomp_eulerian.foata]
sum_inv_cyc_lt_blocks [lemma, in mathcomp_eulerian.foata]
sum_size_belast_wf [lemma, in mathcomp_eulerian.foata]
sum_beta_eq_fact [lemma, in mathcomp_eulerian.beta]
sym_diff [definition, in mathcomp_eulerian.beta_omega]
sym_diff_eq0 [lemma, in mathcomp_eulerian.beta_swap]
sym_diff_toggle_in [lemma, in mathcomp_eulerian.beta_swap]
S_w_seq_decomp_mm [lemma, in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_psi [lemma, in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_bound [lemma, in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_all_lt [lemma, in mathcomp_eulerian.perm_seq_bridge]
S_w_seq_witness_perm [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_map_succ [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_shift [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_witness_k0 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_core [lemma, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex4 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex3 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex2 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex1 [definition, in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq [definition, in mathcomp_eulerian.psi_cdindex_witness]

T

take_mm_psi [lemma, in mathcomp_eulerian.psi_core]
take_psi_perm [lemma, in mathcomp_eulerian.psi_core]
take_psi [lemma, in mathcomp_eulerian.psi_core]
take_mm_eq [lemma, in mathcomp_eulerian.psi_descent_v2]
tcs_12345 [definition, in mathcomp_eulerian.altsub]
tcs_321 [definition, in mathcomp_eulerian.altsub]
tcs_3142 [definition, in mathcomp_eulerian.altsub]
tcs_312 [definition, in mathcomp_eulerian.altsub]
toggle_at_j_omega_strict_superset [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_j_omega_bit_i_new [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_omega_strict_superset [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_omega_bit_i_new [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_other [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_self [lemma, in mathcomp_eulerian.beta_omega]
toggle_atK [lemma, in mathcomp_eulerian.beta_omega]
toggle_at_in [lemma, in mathcomp_eulerian.beta_omega]
toggle_at [definition, in mathcomp_eulerian.beta_omega]
toggle_at_compl [lemma, in mathcomp_eulerian.beta_swap]
transitions_expand_cde_mem [lemma, in mathcomp_eulerian.psi_cdindex_support_defs]
tree_structure [lemma, in mathcomp_eulerian.psi_descent_v2]
tree_structure_via_tree [lemma, in mathcomp_eulerian.psi_descent_v2]
tree_props [definition, in mathcomp_eulerian.psi_descent_v2]
triangle_xor_nat [lemma, in mathcomp_eulerian.altsub]
triangle_xor_nat_g [lemma, in mathcomp_eulerian.altsub]
triple_flip_pos_seq [lemma, in mathcomp_eulerian.altsub]
TurnDefs [section, in mathcomp_eulerian.altsub]
TurnDefs.n [variable, in mathcomp_eulerian.altsub]
TurnLemmas [section, in mathcomp_eulerian.altsub]
TurnLemmas.n [variable, in mathcomp_eulerian.altsub]
turn_image_lt_max [lemma, in mathcomp_eulerian.altsub]
turn_witness [definition, in mathcomp_eulerian.altsub]
turn_inj_inj [lemma, in mathcomp_eulerian.altsub]
turn_inj [definition, in mathcomp_eulerian.altsub]
turn_iv_split [lemma, in mathcomp_eulerian.altsub]
turn_iv_subset [lemma, in mathcomp_eulerian.altsub]
turn_iv [definition, in mathcomp_eulerian.altsub]
turn_count_seq_pair [lemma, in mathcomp_eulerian.altsub]
turn_count_seq_singleton [lemma, in mathcomp_eulerian.altsub]
turn_count_seq_nil [lemma, in mathcomp_eulerian.altsub]
turn_count_seq [definition, in mathcomp_eulerian.altsub]
turn_count_max_iff [lemma, in mathcomp_eulerian.altsub]
turn_count_alt_desc [lemma, in mathcomp_eulerian.altsub]
turn_count_id [lemma, in mathcomp_eulerian.altsub]
turn_count_le [lemma, in mathcomp_eulerian.altsub]
turn_count [definition, in mathcomp_eulerian.altsub]

U

uniq_powerset_internal [lemma, in mathcomp_eulerian.psi_cdindex_core]
uniq_powerset_of [lemma, in mathcomp_eulerian.psi_cdindex_core]
uniq_map_char_mono_powerset [lemma, in mathcomp_eulerian.psi_cdindex_support]
uniq_expand_cde [lemma, in mathcomp_eulerian.psi_cdindex_support]
uniq_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_defs]
uniq_set_to_seq [lemma, in mathcomp_eulerian.beta_bridge]
uniq_adj_of_uniq [lemma, in mathcomp_eulerian.altsub]
uniq_adj_head_neq [lemma, in mathcomp_eulerian.altsub]
uniq_adj_tail [lemma, in mathcomp_eulerian.altsub]
uniq_adj_cons2 [lemma, in mathcomp_eulerian.altsub]
uniq_adj [definition, in mathcomp_eulerian.altsub]
uniq_psi [lemma, in mathcomp_eulerian.psi_core]
uniq_rank_shift_seq [lemma, in mathcomp_eulerian.psi_core]
uniq_expand_cde [lemma, in mathcomp_eulerian.perm_seq_bridge]
UnliftOrd [section, in mathcomp_eulerian.ordinal_reindex]
UnliftOrd.n [variable, in mathcomp_eulerian.ordinal_reindex]
UpperBound [section, in mathcomp_eulerian.altsub]
UpperBoundAssembly [section, in mathcomp_eulerian.altsub]
UpperBoundAssembly.n [variable, in mathcomp_eulerian.altsub]
UpperBoundChain [section, in mathcomp_eulerian.altsub]
UpperBoundChain.n [variable, in mathcomp_eulerian.altsub]
UpperBound.n [variable, in mathcomp_eulerian.altsub]

V

valid_mm_build [lemma, in mathcomp_eulerian.psi_descent_v2]
valid_mm [definition, in mathcomp_eulerian.psi_descent_v2]
val_turn_inj [lemma, in mathcomp_eulerian.altsub]

W

wa_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
wa_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
wa_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]
wf_block_decomp [lemma, in mathcomp_eulerian.foata]
wf_block_rcons [lemma, in mathcomp_eulerian.foata]
wf_block [definition, in mathcomp_eulerian.foata]
widenSn_neq_ord_max [lemma, in mathcomp_eulerian.eulerian]
widenSn_inj [lemma, in mathcomp_eulerian.eulerian]
window_size_apply_psis [lemma, in mathcomp_eulerian.psi_cdindex_core]
window_size_psi_ancestor_ex [definition, in mathcomp_eulerian.psi_comm]
window_size_psi_ancestor [lemma, in mathcomp_eulerian.psi_comm]
window_at_psi_disjoint [lemma, in mathcomp_eulerian.psi_comm]
window_size_psi [lemma, in mathcomp_eulerian.psi_comm]
window_at_uniq [lemma, in mathcomp_eulerian.psi_descent_thms]
window_size_of_shape [lemma, in mathcomp_eulerian.psi_cdindex_tree_shape]
window_size_order_iso [lemma, in mathcomp_eulerian.psi_core]
window_trichotomy_ex [definition, in mathcomp_eulerian.psi_core]
window_trichotomy [lemma, in mathcomp_eulerian.psi_core]
window_head_extremum [lemma, in mathcomp_eulerian.psi_core]
window_at_psi_self [lemma, in mathcomp_eulerian.psi_core]
window_size_psi_self [lemma, in mathcomp_eulerian.psi_core]
window_fits_left [lemma, in mathcomp_eulerian.psi_core]
window_at_cons [lemma, in mathcomp_eulerian.psi_core]
window_size_cons [lemma, in mathcomp_eulerian.psi_core]
window_size_fuel_monotone [lemma, in mathcomp_eulerian.psi_core]
window_size_oor [lemma, in mathcomp_eulerian.psi_core]
window_size_bound [lemma, in mathcomp_eulerian.psi_core]
window_size_gt0 [lemma, in mathcomp_eulerian.psi_core]
window_size_fuel_bound [lemma, in mathcomp_eulerian.psi_core]
window_at [definition, in mathcomp_eulerian.psi_core]
window_size [definition, in mathcomp_eulerian.psi_core]
window_size_fuel [definition, in mathcomp_eulerian.psi_core]
window_size_bound [lemma, in mathcomp_eulerian.perm_seq_bridge]
window_size_t_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_gt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_eq [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_lt [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_t [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_last [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_last_fuel [lemma, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex3 [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex2 [definition, in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex1 [definition, in mathcomp_eulerian.psi_cdindex_tree]
witness_perm_uniq [lemma, in mathcomp_eulerian.psi_cdindex_witness]
witness_perm [definition, in mathcomp_eulerian.psi_cdindex_witness]
worpitzky [lemma, in mathcomp_eulerian.eulerian]
worpitzky_binom_id [lemma, in mathcomp_eulerian.eulerian]
ws_lt_size [lemma, in mathcomp_eulerian.psi_core]
ws_core_1 [lemma, in mathcomp_eulerian.psi_cdindex_witness]
ws_bridge_right [lemma, in mathcomp_eulerian.psi_descent_v2]
ws_bridge_root [lemma, in mathcomp_eulerian.psi_descent_v2]
ws_bridge_left [lemma, in mathcomp_eulerian.psi_descent_v2]

X

xone_desc_eq [lemma, in mathcomp_eulerian.psi_descent_v2]

other

σ [abbreviation, in mathcomp_eulerian.qfact]

Variable Index

A

AltDesc.n [in mathcomp_eulerian.altsub]
AsPermMaxBoundsM.n [in mathcomp_eulerian.altsub]
AsPermMaxBounds.n [in mathcomp_eulerian.altsub]

B

Bridges.Hmm [in mathcomp_eulerian.psi_descent_v2]
Bridges.s [in mathcomp_eulerian.psi_descent_v2]
Bridges.sl [in mathcomp_eulerian.psi_descent_v2]
Bridges.sr [in mathcomp_eulerian.psi_descent_v2]
Bridges.x [in mathcomp_eulerian.psi_descent_v2]

C

Cancellation.n [in mathcomp_eulerian.perm_compress]
CycleCountInsertAfter.j0 [in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.n [in mathcomp_eulerian.stirling_fiber]
CycleCountInsertAfter.s [in mathcomp_eulerian.stirling_fiber]

D

DescentDrop.n [in mathcomp_eulerian.descent]
DescentReverse.n [in mathcomp_eulerian.descent]
Descent.n [in mathcomp_eulerian.descent]
DesInsertMax.n [in mathcomp_eulerian.eulerian]
DesInsertMax.t [in mathcomp_eulerian.eulerian]
DropPerm.n [in mathcomp_eulerian.perm_compress]
DropPerm.s [in mathcomp_eulerian.perm_compress]

E

Equidistribution.FoataPerm.n [in mathcomp_eulerian.foata]
ExistenceLB.n [in mathcomp_eulerian.altsub]
ExtractMax.n [in mathcomp_eulerian.eulerian]
ExtractMax.p [in mathcomp_eulerian.eulerian]
ExtractMax.s [in mathcomp_eulerian.eulerian]
ExtractMax.sp [in mathcomp_eulerian.eulerian]

F

FoataBlocks.n [in mathcomp_eulerian.beta_omega]

H

H1.n [in mathcomp_eulerian.cycles_rec]
H1.s [in mathcomp_eulerian.cycles_rec]

I

InsertAfter.n [in mathcomp_eulerian.stirling_fiber]
InsertExtractBij.n [in mathcomp_eulerian.eulerian]
InsertMax.n [in mathcomp_eulerian.eulerian]
InsertMax.p [in mathcomp_eulerian.eulerian]
InsertMax.t [in mathcomp_eulerian.eulerian]
InterTurn.n [in mathcomp_eulerian.altsub]
Inversions.n [in mathcomp_eulerian.inversions]
InvInsertMax.n [in mathcomp_eulerian.qfact]
InvInsertMax.p [in mathcomp_eulerian.qfact]
InvInsertMax.t [in mathcomp_eulerian.qfact]
InvMajBoundsRev.n [in mathcomp_eulerian.inversions]

L

LiftOrd.n [in mathcomp_eulerian.ordinal_reindex]
LiftPerm.k [in mathcomp_eulerian.perm_compress]
LiftPerm.n [in mathcomp_eulerian.perm_compress]
LiftPerm.t [in mathcomp_eulerian.perm_compress]
LowerBound.n [in mathcomp_eulerian.altsub]

M

MajorIndex.n [in mathcomp_eulerian.inversions]
MaxAlternation.n [in mathcomp_eulerian.altsub]

P

PickSeqFull.n [in mathcomp_eulerian.altsub]

S

SeqToPerm.Hbnd [in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.Hsz [in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.Huniq [in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.n [in mathcomp_eulerian.perm_seq_bridge]
SeqToPerm.w [in mathcomp_eulerian.perm_seq_bridge]
SignPerm.n [in mathcomp_eulerian.altsub]
SlotInterval.n [in mathcomp_eulerian.altsub]

T

TurnDefs.n [in mathcomp_eulerian.altsub]
TurnLemmas.n [in mathcomp_eulerian.altsub]

U

UnliftOrd.n [in mathcomp_eulerian.ordinal_reindex]
UpperBoundAssembly.n [in mathcomp_eulerian.altsub]
UpperBoundChain.n [in mathcomp_eulerian.altsub]
UpperBound.n [in mathcomp_eulerian.altsub]

Library Index

A

altsub

B

beta
beta_swap
beta_bridge
beta_omega

C

cycles
cycles_rec

D

E

F

foata

I

M

mmtree

O

ordinal_reindex

P

perm_seq_bridge
perm_compress
psi_descent_v2
psi_cdindex_support
psi_comm
psi_cdindex_tree_shape
psi_cdindex_tree_hlc
psi_cdindex_tree
psi_cdindex_defs
psi_descent
psi_core
psi_descent_thms
psi_cdindex_witness
psi_cdindex_core
psi_cdindex_support_defs

Q

qeul
qfact

S

Lemma Index

A

all_bnd_apply_psis [in mathcomp_eulerian.perm_seq_bridge]
all_le_iota' [in mathcomp_eulerian.psi_cdindex_witness]
alt_pair_parity [in mathcomp_eulerian.beta_swap]
alt_desc_set_is_alt [in mathcomp_eulerian.beta_swap]
alt_aux_from_sign [in mathcomp_eulerian.altsub]
alt_aux_size_ge1 [in mathcomp_eulerian.altsub]
alt_aux_cons [in mathcomp_eulerian.altsub]
apply_psis_rcons [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_cat [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_cons [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_nil [in mathcomp_eulerian.psi_cdindex_defs]
apply_psis_size_eq [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_cancel [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_revK [in mathcomp_eulerian.perm_seq_bridge]
apply_psis_rev [in mathcomp_eulerian.perm_seq_bridge]
as_perm_max_eq [in mathcomp_eulerian.altsub]
as_perm_max_upper [in mathcomp_eulerian.altsub]
as_perm_max_lower [in mathcomp_eulerian.altsub]
as_perm_max_full [in mathcomp_eulerian.altsub]
as_perm_max_le_size [in mathcomp_eulerian.altsub]
as_perm_full [in mathcomp_eulerian.altsub]
as_perm_max_ge0 [in mathcomp_eulerian.altsub]
as_perm_alt_desc [in mathcomp_eulerian.altsub]
as_perm_id [in mathcomp_eulerian.altsub]
as_perm_le_size [in mathcomp_eulerian.altsub]
as_perm_ge2 [in mathcomp_eulerian.altsub]
as_permE [in mathcomp_eulerian.altsub]
aux_id [in mathcomp_eulerian.eulerian]
aux_id_step [in mathcomp_eulerian.eulerian]

B

beta_alt_max [in mathcomp_eulerian.beta_swap]
beta_set_is_alt_eq [in mathcomp_eulerian.beta_swap]
beta_compl [in mathcomp_eulerian.beta_swap]
beta_rev [in mathcomp_eulerian.beta]
beta_eulerian [in mathcomp_eulerian.beta]
beta_full [in mathcomp_eulerian.beta]
beta_swap_lt_caseA [in mathcomp_eulerian.perm_seq_bridge]
beta0 [in mathcomp_eulerian.beta]
binS' [in mathcomp_eulerian.eulerian]
block_chain_values [in mathcomp_eulerian.beta_omega]
block_chain_step [in mathcomp_eulerian.beta_omega]
block_right_maximal [in mathcomp_eulerian.beta_omega]
block_left_minimal [in mathcomp_eulerian.beta_omega]
block_left_le_right [in mathcomp_eulerian.beta_omega]
block_descent_chain [in mathcomp_eulerian.beta_omega]
block_right_descent [in mathcomp_eulerian.beta_omega]
block_left_descent [in mathcomp_eulerian.beta_omega]
block_right_ge [in mathcomp_eulerian.beta_omega]
block_left_le [in mathcomp_eulerian.beta_omega]
block_right_max [in mathcomp_eulerian.beta_omega]
block_left_min [in mathcomp_eulerian.beta_omega]
block_right_right_ok [in mathcomp_eulerian.beta_omega]
block_left_left_ok [in mathcomp_eulerian.beta_omega]
bool_triangle [in mathcomp_eulerian.altsub]

C

card_split_ord_pair [in mathcomp_eulerian.inversions]
card_ord_pair [in mathcomp_eulerian.inversions]
card_turn_witness [in mathcomp_eulerian.altsub]
card_turn_image [in mathcomp_eulerian.altsub]
card_turn_iv_le [in mathcomp_eulerian.altsub]
card_slot_iv [in mathcomp_eulerian.altsub]
card_eq_ord_max_fiber [in mathcomp_eulerian.stirling_fiber]
card_neq_ord_max_fiber [in mathcomp_eulerian.stirling_fiber]
cde_total_width_phi_w [in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_phi_w_all [in mathcomp_eulerian.psi_cdindex_support]
cde_total_width_cat [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_D_succ [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_offset_C_succ [in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono_apply_psis_D_bit_self [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_D_bit_pred [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_C_bit [in mathcomp_eulerian.psi_cdindex_core]
char_mono_psi_effect [in mathcomp_eulerian.psi_cdindex_core]
char_mono_apply_psis_inj [in mathcomp_eulerian.psi_cdindex_support]
char_mono_apply_psis_mem [in mathcomp_eulerian.psi_cdindex_support]
char_mono_self_mem [in mathcomp_eulerian.psi_cdindex_support]
char_mono_in_expand_cde [in mathcomp_eulerian.perm_seq_bridge]
char_mono_class_inj [in mathcomp_eulerian.perm_seq_bridge]
char_mono_perm_to_seq [in mathcomp_eulerian.perm_seq_bridge]
check_fact3_size1 [in mathcomp_eulerian.psi_cdindex_core]
check_fact3P [in mathcomp_eulerian.psi_cdindex_core]
check_fact3_true [in mathcomp_eulerian.psi_cdindex_support]
check_fact3_of_perm_eq [in mathcomp_eulerian.psi_cdindex_support]
check_strict_witness_correct [in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_mm [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_right [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_left [in mathcomp_eulerian.psi_cdindex_support]
classify_vertex_cde_psi [in mathcomp_eulerian.psi_cdindex_support]
classify_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
classify_skip_mm0 [in mathcomp_eulerian.psi_cdindex_witness]
class_char_monos_uniq [in mathcomp_eulerian.perm_seq_bridge]
cmp_out_of_range_left [in mathcomp_eulerian.psi_descent_thms]
cmp_out_of_range [in mathcomp_eulerian.psi_descent_thms]
compl_perm_involutive [in mathcomp_eulerian.beta_swap]
compl_perm_inj [in mathcomp_eulerian.beta_swap]
compl_permE [in mathcomp_eulerian.beta_swap]
constant_descent_monotone [in mathcomp_eulerian.altsub]
count_lt_cat [in mathcomp_eulerian.foata]
count_lt_perm_eq [in mathcomp_eulerian.foata]
count_gt_cat [in mathcomp_eulerian.foata]
count_gt_cons [in mathcomp_eulerian.foata]
count_gt_perm_eq [in mathcomp_eulerian.foata]
cross_inv_perm_eq_l [in mathcomp_eulerian.foata]
cross_inv_perm_eq_r [in mathcomp_eulerian.foata]
cross_inv_cat_r [in mathcomp_eulerian.foata]
cross_inv_cat_l [in mathcomp_eulerian.foata]
cross_inv_cons [in mathcomp_eulerian.foata]
cross_inv_rcons [in mathcomp_eulerian.foata]
cross_inv_nil_l [in mathcomp_eulerian.foata]
cross_inv_nil_r [in mathcomp_eulerian.foata]
cycle_count_id [in mathcomp_eulerian.cycles]
cycle_count_le [in mathcomp_eulerian.cycles]
cycle_count_lift_perm_id [in mathcomp_eulerian.cycles_rec]
cycle_count_insert_after [in mathcomp_eulerian.stirling_fiber]
cyc_last_to_front_wf [in mathcomp_eulerian.foata]
cyc_last_to_frontK [in mathcomp_eulerian.foata]
cyc_first_to_backK [in mathcomp_eulerian.foata]
cyc_first_to_back_uniq [in mathcomp_eulerian.foata]
cyc_first_to_back_perm_eq [in mathcomp_eulerian.foata]
cyc_first_to_back_size [in mathcomp_eulerian.foata]
cyc_diff_block_gt [in mathcomp_eulerian.foata]
cyc_diff_block_lt [in mathcomp_eulerian.foata]
cyc_last_to_front_rcons [in mathcomp_eulerian.foata]
cyc_last_to_front_uniq [in mathcomp_eulerian.foata]
cyc_last_to_front_size [in mathcomp_eulerian.foata]
cyc_last_to_front_perm_eq [in mathcomp_eulerian.foata]

D

descent_psi_effect [in mathcomp_eulerian.psi_cdindex_core]
descent_psi_LR_swap2 [in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap1 [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add [in mathcomp_eulerian.psi_descent_thms]
descent_psi_lboundary_R [in mathcomp_eulerian.psi_descent_thms]
descent_psi_rboundary [in mathcomp_eulerian.psi_descent_thms]
descent_psi_interior [in mathcomp_eulerian.psi_descent_thms]
descent_set_compl [in mathcomp_eulerian.beta_swap]
descent_set_full_rev [in mathcomp_eulerian.beta]
descent_set_rev_perm_ord [in mathcomp_eulerian.beta]
descent_set_rev_perm [in mathcomp_eulerian.beta]
descent_to_bvec_inj [in mathcomp_eulerian.perm_seq_bridge]
desc_positions_bvec [in mathcomp_eulerian.perm_seq_bridge]
des_insert_max_interior [in mathcomp_eulerian.eulerian]
des_insert_max_ord_max [in mathcomp_eulerian.eulerian]
des_insert_max_ord0 [in mathcomp_eulerian.eulerian]
des_rev_perm_ord [in mathcomp_eulerian.descent]
des_rev_perm [in mathcomp_eulerian.descent]
des_id [in mathcomp_eulerian.descent]
des_add_asc [in mathcomp_eulerian.descent]
des_le [in mathcomp_eulerian.descent]
des0_id [in mathcomp_eulerian.eulerian]
dir_right_of_turn [in mathcomp_eulerian.altsub]
dir_left_of_turn [in mathcomp_eulerian.altsub]
drop_psi_above [in mathcomp_eulerian.psi_core]
drop_mm_psi [in mathcomp_eulerian.psi_core]
drop_psi [in mathcomp_eulerian.psi_core]
drop_perm_lift_perm [in mathcomp_eulerian.perm_compress]
drop_permE [in mathcomp_eulerian.perm_compress]
drop_fun_inj [in mathcomp_eulerian.perm_compress]
drop_funE [in mathcomp_eulerian.perm_compress]
drop_fun_ne [in mathcomp_eulerian.perm_compress]
drop_mm_eq [in mathcomp_eulerian.psi_descent_v2]
drop1_witness_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
D_vertex_descent_transition [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_phi_w_eq_S_w_seq [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cat_D [in mathcomp_eulerian.psi_cdindex_support]
D_offsets_cons_C [in mathcomp_eulerian.psi_cdindex_support]

E

elem_rs_in_range [in mathcomp_eulerian.psi_descent_thms]
elem_in_range [in mathcomp_eulerian.psi_descent_thms]
endpoint_succ_is_D_internal [in mathcomp_eulerian.psi_cdindex_core]
endpoint_implies_next_has_left_child [in mathcomp_eulerian.psi_cdindex_tree]
endpoint_implies_next_t [in mathcomp_eulerian.psi_cdindex_tree]
enum_ord_split [in mathcomp_eulerian.altsub]
eulerian_explicit [in mathcomp_eulerian.eulerian]
eulerian_rec [in mathcomp_eulerian.eulerian]
eulerian_n_n [in mathcomp_eulerian.eulerian]
eulerian_symm [in mathcomp_eulerian.eulerian]
eulerian_n_0 [in mathcomp_eulerian.eulerian]
eulerian_out_of_range [in mathcomp_eulerian.eulerian]
eulerian_row_sum_fact [in mathcomp_eulerian.eulerian]
eulerian_row_sum [in mathcomp_eulerian.eulerian]
exactly_one_descent_LR [in mathcomp_eulerian.psi_descent_v2]
expand_cde_mem_iff [in mathcomp_eulerian.psi_cdindex_support_defs]
expand_cde_mem_transitions [in mathcomp_eulerian.psi_cdindex_support_defs]
extract_insert_maxPI [in mathcomp_eulerian.eulerian]
extract_insert_max [in mathcomp_eulerian.eulerian]
extract_max_widen [in mathcomp_eulerian.eulerian]
extract_max_permE [in mathcomp_eulerian.eulerian]
extract_max_fun_inj [in mathcomp_eulerian.eulerian]
extract_max_funE [in mathcomp_eulerian.eulerian]
extract_max_ne [in mathcomp_eulerian.eulerian]

F

fact3 [in mathcomp_eulerian.psi_cdindex_support]
find_ss_spec [in mathcomp_eulerian.perm_seq_bridge]
flip_count_perm_seq_eq_turn_count [in mathcomp_eulerian.altsub]
flip_count_as_sum [in mathcomp_eulerian.altsub]
flip_count_pick_le_perm [in mathcomp_eulerian.altsub]
flip_count_is_alt_bool [in mathcomp_eulerian.altsub]
flip_count_sign_seq_le_subseq [in mathcomp_eulerian.altsub]
flip_count_pairmap_le_subseq [in mathcomp_eulerian.altsub]
flip_count_sign_seq_insert_front [in mathcomp_eulerian.altsub]
flip_count_pairmap_insert_anywhere [in mathcomp_eulerian.altsub]
flip_step_helper [in mathcomp_eulerian.altsub]
flip_count_pairmap_insert [in mathcomp_eulerian.altsub]
flip_count_cons2 [in mathcomp_eulerian.altsub]
foata_perm_inj [in mathcomp_eulerian.foata]
foata_perm_inv_maj [in mathcomp_eulerian.foata]
foata_perm_to_seq_bnd [in mathcomp_eulerian.foata]
foata_perm_to_seq_uniq [in mathcomp_eulerian.foata]
foata_perm_to_seq_size [in mathcomp_eulerian.foata]
foata_inj_uniq [in mathcomp_eulerian.foata]
foata_invK [in mathcomp_eulerian.foata]
foata_invK_aux [in mathcomp_eulerian.foata]
foata_step_undoK [in mathcomp_eulerian.foata]
foata_inv_eq_maj [in mathcomp_eulerian.foata]
foata_step_inv [in mathcomp_eulerian.foata]
foata_step_inv_gt [in mathcomp_eulerian.foata]
foata_step_inv_lt [in mathcomp_eulerian.foata]
foata_last_eq [in mathcomp_eulerian.foata]
foata_last [in mathcomp_eulerian.foata]
foata_rcons [in mathcomp_eulerian.foata]
foata_step_last [in mathcomp_eulerian.foata]
foata_all_lt [in mathcomp_eulerian.foata]
foata_uniq [in mathcomp_eulerian.foata]
foata_size [in mathcomp_eulerian.foata]
foata_perm_eq [in mathcomp_eulerian.foata]
foata_step_uniq [in mathcomp_eulerian.foata]
foata_step_size [in mathcomp_eulerian.foata]
foata_step_perm_eq [in mathcomp_eulerian.foata]
foldr_maxn_set_to_seq_lb [in mathcomp_eulerian.beta_bridge]
foldr_maxn_ge [in mathcomp_eulerian.psi_cdindex_support_defs]
foldr_maxn_ge_nth [in mathcomp_eulerian.psi_core]
foldr_minn_le_nth [in mathcomp_eulerian.psi_core]
foldr_maxn_ge [in mathcomp_eulerian.psi_core]
foldr_maxn_aux [in mathcomp_eulerian.psi_core]
foldr_minn_le [in mathcomp_eulerian.psi_core]
foldr_minn_aux [in mathcomp_eulerian.psi_core]
foldr_minn_all_gt' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_iota' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_minn_ge' [in mathcomp_eulerian.psi_cdindex_witness]
foldr_maxn_path' [in mathcomp_eulerian.psi_cdindex_witness]

G

geq_minn' [in mathcomp_eulerian.psi_cdindex_witness]
geq_maxn' [in mathcomp_eulerian.psi_cdindex_witness]

H

has_left_child_is_internal [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last_fuel [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_last [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_t_last_valid [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
has_left_child_psi [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_order_iso [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_left_child_of_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
has_transition_omega_seq [in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons2 [in mathcomp_eulerian.psi_cdindex_support_defs]
has_transition_cons [in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t_eq [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_0 [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_gt [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_eq [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_t_Node_lt [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_iota [in mathcomp_eulerian.psi_cdindex_witness]
has_left_child_cons [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_monotone [in mathcomp_eulerian.psi_descent_v2]
has_left_child_0 [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel_0 [in mathcomp_eulerian.psi_descent_v2]
head_max_is_descent [in mathcomp_eulerian.psi_descent_thms]
head_min_not_descent [in mathcomp_eulerian.psi_descent_thms]
head_rank_shift_seq [in mathcomp_eulerian.psi_core]
hlc_core_1 [in mathcomp_eulerian.psi_cdindex_witness]
hlc_core_not1 [in mathcomp_eulerian.psi_cdindex_witness]
hlc_bridge_right [in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_root [in mathcomp_eulerian.psi_descent_v2]
hlc_bridge_left [in mathcomp_eulerian.psi_descent_v2]

I

imset_rev_ord_compl [in mathcomp_eulerian.beta]
imset_rev_ord_inv [in mathcomp_eulerian.beta]
index_rcons_eq_size [in mathcomp_eulerian.psi_cdindex_core]
index_map_inj_in [in mathcomp_eulerian.psi_comm]
index_lt_sorted [in mathcomp_eulerian.perm_seq_bridge]
insert_max_perm_bij [in mathcomp_eulerian.eulerian]
insert_max_perm_pair_surj [in mathcomp_eulerian.eulerian]
insert_max_perm_pair_inj [in mathcomp_eulerian.eulerian]
insert_max_perm_fiber [in mathcomp_eulerian.eulerian]
insert_extract_max [in mathcomp_eulerian.eulerian]
insert_max_perm_lift [in mathcomp_eulerian.eulerian]
insert_max_perm_at_p [in mathcomp_eulerian.eulerian]
insert_max_permE [in mathcomp_eulerian.eulerian]
insert_max_fun_inj [in mathcomp_eulerian.eulerian]
insert_max_fun_lift [in mathcomp_eulerian.eulerian]
insert_max_fun_p [in mathcomp_eulerian.eulerian]
insert_after_surj [in mathcomp_eulerian.stirling_fiber]
insert_after_inj_pair [in mathcomp_eulerian.stirling_fiber]
insert_after_decomp [in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max_neq [in mathcomp_eulerian.stirling_fiber]
insert_after_other [in mathcomp_eulerian.stirling_fiber]
insert_after_j0 [in mathcomp_eulerian.stirling_fiber]
insert_after_ord_max [in mathcomp_eulerian.stirling_fiber]
insert_afterE [in mathcomp_eulerian.stirling_fiber]
insert_after_fun_inj [in mathcomp_eulerian.stirling_fiber]
interior_val_bounds [in mathcomp_eulerian.altsub]
interior_is_turn_inj [in mathcomp_eulerian.altsub]
internal_vertices_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
inter_turn_monotone_strict [in mathcomp_eulerian.altsub]
inter_turn_monotone [in mathcomp_eulerian.altsub]
inv_rev_perm [in mathcomp_eulerian.inversions]
inv_rev_perm_eq_coinv [in mathcomp_eulerian.inversions]
inv_le [in mathcomp_eulerian.inversions]
inv_double_sum [in mathcomp_eulerian.inversions]
inv_id [in mathcomp_eulerian.inversions]
inv_q_fact [in mathcomp_eulerian.qfact]
inv_insert_max [in mathcomp_eulerian.qfact]
inv_via_sum [in mathcomp_eulerian.qfact]
inv_maj_equidistr [in mathcomp_eulerian.foata]
inv_eq_inv_seq [in mathcomp_eulerian.foata]
inv_seq_cons_eq_rcons_shift [in mathcomp_eulerian.foata]
inv_seq_flatten_swap_eq [in mathcomp_eulerian.foata]
inv_seq_cat [in mathcomp_eulerian.foata]
inv_seq_rcons [in mathcomp_eulerian.foata]
in_internal_vertices [in mathcomp_eulerian.psi_cdindex_support]
iota_mem_range [in mathcomp_eulerian.psi_cdindex_witness]
is_internal_lt [in mathcomp_eulerian.psi_cdindex_core]
is_internal_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
is_inv_lift_p [in mathcomp_eulerian.qfact]
is_inv_p_lift [in mathcomp_eulerian.qfact]
is_inv_lift_pair [in mathcomp_eulerian.qfact]
is_descent_compl [in mathcomp_eulerian.beta_swap]
is_descent_rev [in mathcomp_eulerian.descent]
is_descent_drop [in mathcomp_eulerian.descent]
is_descentE [in mathcomp_eulerian.descent]
is_alt_pick_turn_witness [in mathcomp_eulerian.altsub]
is_alt_from_sign [in mathcomp_eulerian.altsub]
is_alt_flip_count [in mathcomp_eulerian.altsub]
is_alt_subseq_strictmono_le2 [in mathcomp_eulerian.altsub]
is_alt_three [in mathcomp_eulerian.altsub]
is_alt_size_le1 [in mathcomp_eulerian.altsub]
is_alt_pick_seq_le2 [in mathcomp_eulerian.altsub]
is_alt_tail [in mathcomp_eulerian.altsub]
is_alt_cons2 [in mathcomp_eulerian.altsub]
is_alt_singleton [in mathcomp_eulerian.altsub]
is_alt_nil [in mathcomp_eulerian.altsub]
is_turnE [in mathcomp_eulerian.altsub]
is_descent_perm_seq [in mathcomp_eulerian.perm_seq_bridge]
is_internal_t_eq [in mathcomp_eulerian.psi_cdindex_tree]

L

last_vertex_internal [in mathcomp_eulerian.psi_cdindex_core]
last_iota' [in mathcomp_eulerian.psi_cdindex_witness]
left_ok_self [in mathcomp_eulerian.beta_omega]
leq_seqb_anti [in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_trans [in mathcomp_eulerian.psi_cdindex_core]
leq_seqb_total [in mathcomp_eulerian.psi_cdindex_core]
leq_lift [in mathcomp_eulerian.ordinal_reindex]
leq_maxn' [in mathcomp_eulerian.psi_cdindex_witness]
lift_image [in mathcomp_eulerian.ordinal_reindex]
lift_perm_id_iter_lift [in mathcomp_eulerian.cycles_rec]
lift_perm_id_iter [in mathcomp_eulerian.cycles_rec]
lift_perm_ord_max_eq [in mathcomp_eulerian.perm_compress]
lift_perm_drop_perm [in mathcomp_eulerian.perm_compress]
lift_perm_ne_k [in mathcomp_eulerian.perm_compress]
lift_perm_lift [in mathcomp_eulerian.perm_compress]
lift_perm_ord_max [in mathcomp_eulerian.perm_compress]
lift_permE [in mathcomp_eulerian.perm_compress]
lift_fun_inj [in mathcomp_eulerian.perm_compress]
lift_fun_lift [in mathcomp_eulerian.perm_compress]
lift_fun_ord_max [in mathcomp_eulerian.perm_compress]
lift_drop_permE [in mathcomp_eulerian.perm_compress]
LR_pred_is_endpoint [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_t [in mathcomp_eulerian.psi_cdindex_tree]
ltn_unlift_some [in mathcomp_eulerian.ordinal_reindex]
ltn_lift [in mathcomp_eulerian.ordinal_reindex]

M

maj_rev_perm [in mathcomp_eulerian.inversions]
maj_le [in mathcomp_eulerian.inversions]
maj_id [in mathcomp_eulerian.inversions]
maj_q_fact [in mathcomp_eulerian.qfact]
maj_eq_maj_seq [in mathcomp_eulerian.foata]
maj_seq_rcons [in mathcomp_eulerian.foata]
map_mod_iota_rot [in mathcomp_eulerian.psi_core]
map_nth_iota_sorted [in mathcomp_eulerian.psi_core]
map_succ_order_iso [in mathcomp_eulerian.psi_cdindex_witness]
max_eq_nth_sort_last [in mathcomp_eulerian.psi_core]
max_val_drop [in mathcomp_eulerian.psi_core]
max_val_perm_eq [in mathcomp_eulerian.psi_core]
max_pos_lt [in mathcomp_eulerian.psi_core]
max_in [in mathcomp_eulerian.psi_core]
max_pos_core_gt0 [in mathcomp_eulerian.psi_cdindex_witness]
max_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
mem_inv_set [in mathcomp_eulerian.inversions]
mem_omega_set [in mathcomp_eulerian.beta_omega]
mem_set_to_seq_ord [in mathcomp_eulerian.beta_bridge]
mem_set_to_seq_iff [in mathcomp_eulerian.beta_bridge]
mem_set_to_seq [in mathcomp_eulerian.beta_bridge]
mem_alt_desc_set [in mathcomp_eulerian.beta_swap]
mem_descent_set [in mathcomp_eulerian.descent]
mem_pos_seq [in mathcomp_eulerian.altsub]
mem_turn_iv [in mathcomp_eulerian.altsub]
mem_slot_iv [in mathcomp_eulerian.altsub]
mem_omega_seq [in mathcomp_eulerian.psi_cdindex_support_defs]
mem_filter_iota_nth [in mathcomp_eulerian.psi_cdindex_support_defs]
min_pos_lt [in mathcomp_eulerian.mmtree]
min_in [in mathcomp_eulerian.mmtree]
min_eq_nth_sort_0 [in mathcomp_eulerian.psi_core]
min_val_drop [in mathcomp_eulerian.psi_core]
min_val_perm_eq [in mathcomp_eulerian.psi_core]
min_pos_core [in mathcomp_eulerian.psi_cdindex_witness]
min_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
mmtree_shape_psi [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_decompose [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_order_iso [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_cons [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_nil [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel_monotone [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seqK [in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel_correct [in mathcomp_eulerian.mmtree]
mmtree_of_seq_mmK [in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel_correct [in mathcomp_eulerian.psi_core]
mm_pos_rcons_lt [in mathcomp_eulerian.psi_cdindex_core]
mm_pos_lt_pred [in mathcomp_eulerian.psi_cdindex_support]
mm_pos_drop_mm [in mathcomp_eulerian.psi_core]
mm_pos_order_iso [in mathcomp_eulerian.psi_core]
mm_pos_psi_eq [in mathcomp_eulerian.psi_core]
mm_pos_char [in mathcomp_eulerian.psi_core]
mm_pos_lt [in mathcomp_eulerian.psi_core]
mm_pos_witness [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_core [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_min_first [in mathcomp_eulerian.psi_cdindex_witness]
mm_pos_iota' [in mathcomp_eulerian.psi_cdindex_witness]
mono_inj_in [in mathcomp_eulerian.psi_comm]

N

neg_add_neg [in mathcomp_eulerian.altsub]
nil_in_powerset_internal [in mathcomp_eulerian.perm_seq_bridge]
notin_take_mm [in mathcomp_eulerian.psi_core]
not_set_is_alt_omega_not_full [in mathcomp_eulerian.beta_swap]
not_set_is_alt_n_ge2 [in mathcomp_eulerian.beta_swap]
not_is_descentE [in mathcomp_eulerian.altsub]
no_inner_in_pos_seq [in mathcomp_eulerian.altsub]
nth_char_mono [in mathcomp_eulerian.psi_cdindex_core]
nth_window_at [in mathcomp_eulerian.psi_descent_thms]
nth_w_mm_pos [in mathcomp_eulerian.psi_core]
nth_psi_inside [in mathcomp_eulerian.psi_core]
nth_psi_right [in mathcomp_eulerian.psi_core]
nth_psi_left [in mathcomp_eulerian.psi_core]
nth_rank_shift_seq [in mathcomp_eulerian.psi_core]
nth_descent_to_bvec [in mathcomp_eulerian.perm_seq_bridge]
nth_perm_to_seq [in mathcomp_eulerian.perm_seq_bridge]

O

omega_set_seq_local_bridge [in mathcomp_eulerian.beta_bridge]
omega_set_alt_full [in mathcomp_eulerian.beta_swap]
omega_proper_beta_lt [in mathcomp_eulerian.perm_seq_bridge]
omega_seq_subset_bounded [in mathcomp_eulerian.perm_seq_bridge]
omega_set_seq_bridge_bounded [in mathcomp_eulerian.perm_seq_bridge]
omega_seq_mem_eq [in mathcomp_eulerian.perm_seq_bridge]
omega_monotone_class_count [in mathcomp_eulerian.psi_cdindex_witness]
order_iso_drop [in mathcomp_eulerian.psi_core]
order_iso_take [in mathcomp_eulerian.psi_core]
ord_max_notin_turn_image [in mathcomp_eulerian.altsub]
ord0_neq_ord_max [in mathcomp_eulerian.altsub]
ord0_notin_turn_image [in mathcomp_eulerian.altsub]

P

path_iota' [in mathcomp_eulerian.psi_cdindex_witness]
path_leq_last' [in mathcomp_eulerian.psi_cdindex_witness]
perm_eq_from_subset [in mathcomp_eulerian.psi_cdindex_support]
perm_eq_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
perm_to_seq_foata_perm [in mathcomp_eulerian.foata]
perm_eq_flatten_map_pred [in mathcomp_eulerian.foata]
perm_eq_flatten_map_cyc [in mathcomp_eulerian.foata]
perm_to_seq_class_map [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_seq_to_perm [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_bnd [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_inj [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_uniq [in mathcomp_eulerian.perm_seq_bridge]
perm_to_seq_size [in mathcomp_eulerian.perm_seq_bridge]
phi_w_as_map [in mathcomp_eulerian.psi_cdindex_core]
phi_w_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
phi_w_support_general [in mathcomp_eulerian.psi_cdindex_support]
phi_w_decomp_mm [in mathcomp_eulerian.psi_cdindex_support]
phi_w_cons_mm0 [in mathcomp_eulerian.psi_cdindex_support]
pick_seq_subseq_perm_seq [in mathcomp_eulerian.altsub]
pick_seq_pos_seq [in mathcomp_eulerian.altsub]
pick_flip_has_turn [in mathcomp_eulerian.altsub]
pick_seq_setT [in mathcomp_eulerian.altsub]
porbits_lift_perm_id [in mathcomp_eulerian.cycles_rec]
porbit_id_singleton [in mathcomp_eulerian.cycles]
porbit_lift_perm_id_lift [in mathcomp_eulerian.cycles_rec]
porbit_lift_perm_id_max [in mathcomp_eulerian.cycles_rec]
post_window_extremum [in mathcomp_eulerian.psi_descent_v2]
pos_seq_last_val [in mathcomp_eulerian.altsub]
pos_seq_nth0 [in mathcomp_eulerian.altsub]
pos_seq_val_lt_inv [in mathcomp_eulerian.altsub]
pos_seq_val_lt [in mathcomp_eulerian.altsub]
pos_seq_strict_sorted [in mathcomp_eulerian.altsub]
pos_seq_uniq [in mathcomp_eulerian.altsub]
powerset_internal_apply_psis [in mathcomp_eulerian.perm_seq_bridge]
pred_sub_add [in mathcomp_eulerian.psi_descent_v2]
pre_window_extremum_R [in mathcomp_eulerian.psi_descent_v2]
pre_window_gt_min_when_max_head [in mathcomp_eulerian.psi_descent_v2]
pre_window_lt_max_when_min_head [in mathcomp_eulerian.psi_descent_v2]
pre_win_gt_min_eq [in mathcomp_eulerian.psi_descent_v2]
pre_win_lt_max_eq [in mathcomp_eulerian.psi_descent_v2]
psi_comm [in mathcomp_eulerian.psi_comm]
psi_comm_nested [in mathcomp_eulerian.psi_comm]
psi_map_comm [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_lr [in mathcomp_eulerian.psi_comm]
psi_0_eq [in mathcomp_eulerian.psi_core]
psi_involutive [in mathcomp_eulerian.psi_core]
psi_id_trivial [in mathcomp_eulerian.psi_core]
psi_id_oor [in mathcomp_eulerian.psi_core]
psi_perm_eq [in mathcomp_eulerian.psi_core]
psi_apply_psis_comm [in mathcomp_eulerian.perm_seq_bridge]

Q

q_eul_pol_q1 [in mathcomp_eulerian.qeul]
q_eul_pol_t1 [in mathcomp_eulerian.qeul]

R

rank_shift_psi_comm [in mathcomp_eulerian.psi_comm]
rank_shift_map_comm [in mathcomp_eulerian.psi_comm]
rank_shift_preserves_interior_order [in mathcomp_eulerian.psi_comm]
rank_shift_head_max_to_min [in mathcomp_eulerian.psi_core]
rank_shift_head_min_to_max [in mathcomp_eulerian.psi_core]
rank_shift_seq_involutive [in mathcomp_eulerian.psi_core]
rank_shift_seqE [in mathcomp_eulerian.psi_core]
rank_shift_perm_eq [in mathcomp_eulerian.psi_core]
rev_ord_lt [in mathcomp_eulerian.inversions]
rev_perm_involutive [in mathcomp_eulerian.eulerian]
rev_perm_inj [in mathcomp_eulerian.eulerian]
rev_permE [in mathcomp_eulerian.descent]
rev_perm_ordE [in mathcomp_eulerian.descent]
right_ok_self [in mathcomp_eulerian.beta_omega]
rs_head_min_no_descent [in mathcomp_eulerian.psi_descent_thms]
rs_head_max_descent [in mathcomp_eulerian.psi_descent_thms]

S

sanity_inv_eq_maj3 [in mathcomp_eulerian.foata]
sanity_inv_eq_maj2 [in mathcomp_eulerian.foata]
sanity_inv_eq_maj [in mathcomp_eulerian.foata]
sanity_insert_after_pointwise [in mathcomp_eulerian.stirling_fiber]
seq_cat_right_eq [in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_cat_left_eq [in mathcomp_eulerian.psi_cdindex_tree_shape]
seq_to_perm_perm_to_seq [in mathcomp_eulerian.perm_seq_bridge]
seq_to_perm_nth [in mathcomp_eulerian.perm_seq_bridge]
seq_to_fun_inj [in mathcomp_eulerian.perm_seq_bridge]
seq_nth_bound [in mathcomp_eulerian.perm_seq_bridge]
set_to_seq_bound [in mathcomp_eulerian.beta_bridge]
set_is_alt_classify [in mathcomp_eulerian.beta_swap]
set_not_altP [in mathcomp_eulerian.beta_swap]
shift_preserves_ltn [in mathcomp_eulerian.psi_comm]
sign_seq_alt_of_triple_flip [in mathcomp_eulerian.altsub]
sign_pair_neq [in mathcomp_eulerian.altsub]
sign_flip_at_turn [in mathcomp_eulerian.altsub]
sign_seq_is_alt [in mathcomp_eulerian.altsub]
sign_seq_perm_seq [in mathcomp_eulerian.altsub]
sign_seq_cons2 [in mathcomp_eulerian.altsub]
size_expand_cde_phi_w [in mathcomp_eulerian.psi_cdindex_core]
size_phi_w [in mathcomp_eulerian.psi_cdindex_core]
size_expand_cde [in mathcomp_eulerian.psi_cdindex_core]
size_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
size_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
size_char_mono [in mathcomp_eulerian.psi_cdindex_core]
size_window_at [in mathcomp_eulerian.psi_descent_thms]
size_mmtree_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
size_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
size_count_lt_gt [in mathcomp_eulerian.foata]
size_pos_seq [in mathcomp_eulerian.altsub]
size_take_drop_skip [in mathcomp_eulerian.altsub]
size_sign_seq_perm [in mathcomp_eulerian.altsub]
size_sign_seq [in mathcomp_eulerian.altsub]
size_perm_seq [in mathcomp_eulerian.altsub]
size_in_expand_cde [in mathcomp_eulerian.psi_cdindex_support_defs]
size_psi [in mathcomp_eulerian.psi_core]
size_rank_shift_seq2 [in mathcomp_eulerian.psi_core]
size_rank_shift_seq [in mathcomp_eulerian.psi_core]
size_descent_to_bvec [in mathcomp_eulerian.perm_seq_bridge]
size_mmtree_to_seq_node [in mathcomp_eulerian.psi_cdindex_tree]
size_witness_perm [in mathcomp_eulerian.psi_cdindex_witness]
slot_descent_const_strict [in mathcomp_eulerian.altsub]
slot_descent_const [in mathcomp_eulerian.altsub]
sorted_uniq_nth_ltn [in mathcomp_eulerian.psi_comm]
sorted_val_enum_ord [in mathcomp_eulerian.altsub]
sorted_last_ge [in mathcomp_eulerian.psi_core]
sorted_head_le [in mathcomp_eulerian.psi_core]
sort_perm_eq_leq_seqb [in mathcomp_eulerian.psi_cdindex_core]
sort_map_mono [in mathcomp_eulerian.psi_comm]
sort_enum_subseq_enum [in mathcomp_eulerian.altsub]
sort_enum_strict_sorted [in mathcomp_eulerian.altsub]
sort_rank_shift_seq [in mathcomp_eulerian.psi_core]
split_blocks_inv_eq [in mathcomp_eulerian.foata]
split_blocks_inv_aux_eq [in mathcomp_eulerian.foata]
split_blocks_inv_cyc_wf [in mathcomp_eulerian.foata]
split_blocks_inv_aux_block_then_P [in mathcomp_eulerian.foata]
split_blocks_inv_aux_one_block [in mathcomp_eulerian.foata]
split_blocks_inv_aux_app_notP [in mathcomp_eulerian.foata]
split_blocks_inv_aux_cons_notP [in mathcomp_eulerian.foata]
split_blocks_inv_aux_cons_P [in mathcomp_eulerian.foata]
split_blocks_inv_flatten [in mathcomp_eulerian.foata]
split_blocks_inv_aux_flatten [in mathcomp_eulerian.foata]
split_blocks_gt_strict [in mathcomp_eulerian.foata]
split_blocks_lt_strict [in mathcomp_eulerian.foata]
split_blocks_size_eq [in mathcomp_eulerian.foata]
split_blocks_aux_size_when_last_P [in mathcomp_eulerian.foata]
split_blocks_wf [in mathcomp_eulerian.foata]
split_blocks_aux_wf [in mathcomp_eulerian.foata]
split_blocks_all_nonempty [in mathcomp_eulerian.foata]
split_blocks_aux_all_nonempty [in mathcomp_eulerian.foata]
split_blocks_flatten [in mathcomp_eulerian.foata]
split_blocks_aux_flatten [in mathcomp_eulerian.foata]
stirling_c_row_sum_fact [in mathcomp_eulerian.cycles]
stirling_c_row_sum [in mathcomp_eulerian.cycles]
stirling_c_rec [in mathcomp_eulerian.stirling_fiber]
strict_witness_exists [in mathcomp_eulerian.psi_cdindex_witness]
subseq_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
subseq_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
subseq_drop_extra [in mathcomp_eulerian.altsub]
subset_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
subset_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
sum_succ_ord_eq_bin2 [in mathcomp_eulerian.inversions]
sum_ascent [in mathcomp_eulerian.eulerian]
sum_descent [in mathcomp_eulerian.eulerian]
sum_geq_p [in mathcomp_eulerian.qfact]
sum_rev_X [in mathcomp_eulerian.qfact]
sum_des_eq_eul_pol [in mathcomp_eulerian.qeul]
sum_inv_cyc_gt_blocks [in mathcomp_eulerian.foata]
sum_inv_cyc_lt_blocks [in mathcomp_eulerian.foata]
sum_size_belast_wf [in mathcomp_eulerian.foata]
sum_beta_eq_fact [in mathcomp_eulerian.beta]
sym_diff_eq0 [in mathcomp_eulerian.beta_swap]
sym_diff_toggle_in [in mathcomp_eulerian.beta_swap]
S_w_seq_decomp_mm [in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_psi [in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_bound [in mathcomp_eulerian.psi_cdindex_support]
S_w_seq_all_lt [in mathcomp_eulerian.perm_seq_bridge]
S_w_seq_witness_perm [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_map_succ [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_shift [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_witness_k0 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_core [in mathcomp_eulerian.psi_cdindex_witness]

T

take_mm_psi [in mathcomp_eulerian.psi_core]
take_psi_perm [in mathcomp_eulerian.psi_core]
take_psi [in mathcomp_eulerian.psi_core]
take_mm_eq [in mathcomp_eulerian.psi_descent_v2]
toggle_at_j_omega_strict_superset [in mathcomp_eulerian.beta_omega]
toggle_at_j_omega_bit_i_new [in mathcomp_eulerian.beta_omega]
toggle_at_omega_strict_superset [in mathcomp_eulerian.beta_omega]
toggle_at_omega_bit_i_new [in mathcomp_eulerian.beta_omega]
toggle_at_other [in mathcomp_eulerian.beta_omega]
toggle_at_self [in mathcomp_eulerian.beta_omega]
toggle_atK [in mathcomp_eulerian.beta_omega]
toggle_at_in [in mathcomp_eulerian.beta_omega]
toggle_at_compl [in mathcomp_eulerian.beta_swap]
transitions_expand_cde_mem [in mathcomp_eulerian.psi_cdindex_support_defs]
tree_structure [in mathcomp_eulerian.psi_descent_v2]
tree_structure_via_tree [in mathcomp_eulerian.psi_descent_v2]
triangle_xor_nat [in mathcomp_eulerian.altsub]
triangle_xor_nat_g [in mathcomp_eulerian.altsub]
triple_flip_pos_seq [in mathcomp_eulerian.altsub]
turn_image_lt_max [in mathcomp_eulerian.altsub]
turn_inj_inj [in mathcomp_eulerian.altsub]
turn_iv_split [in mathcomp_eulerian.altsub]
turn_iv_subset [in mathcomp_eulerian.altsub]
turn_count_seq_pair [in mathcomp_eulerian.altsub]
turn_count_seq_singleton [in mathcomp_eulerian.altsub]
turn_count_seq_nil [in mathcomp_eulerian.altsub]
turn_count_max_iff [in mathcomp_eulerian.altsub]
turn_count_alt_desc [in mathcomp_eulerian.altsub]
turn_count_id [in mathcomp_eulerian.altsub]
turn_count_le [in mathcomp_eulerian.altsub]

U

uniq_powerset_internal [in mathcomp_eulerian.psi_cdindex_core]
uniq_powerset_of [in mathcomp_eulerian.psi_cdindex_core]
uniq_map_char_mono_powerset [in mathcomp_eulerian.psi_cdindex_support]
uniq_expand_cde [in mathcomp_eulerian.psi_cdindex_support]
uniq_apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
uniq_set_to_seq [in mathcomp_eulerian.beta_bridge]
uniq_adj_of_uniq [in mathcomp_eulerian.altsub]
uniq_adj_head_neq [in mathcomp_eulerian.altsub]
uniq_adj_tail [in mathcomp_eulerian.altsub]
uniq_adj_cons2 [in mathcomp_eulerian.altsub]
uniq_psi [in mathcomp_eulerian.psi_core]
uniq_rank_shift_seq [in mathcomp_eulerian.psi_core]
uniq_expand_cde [in mathcomp_eulerian.perm_seq_bridge]

V

valid_mm_build [in mathcomp_eulerian.psi_descent_v2]
val_turn_inj [in mathcomp_eulerian.altsub]

W

wa_bridge_right [in mathcomp_eulerian.psi_descent_v2]
wa_bridge_root [in mathcomp_eulerian.psi_descent_v2]
wa_bridge_left [in mathcomp_eulerian.psi_descent_v2]
wf_block_decomp [in mathcomp_eulerian.foata]
wf_block_rcons [in mathcomp_eulerian.foata]
widenSn_neq_ord_max [in mathcomp_eulerian.eulerian]
widenSn_inj [in mathcomp_eulerian.eulerian]
window_size_apply_psis [in mathcomp_eulerian.psi_cdindex_core]
window_size_psi_ancestor [in mathcomp_eulerian.psi_comm]
window_at_psi_disjoint [in mathcomp_eulerian.psi_comm]
window_size_psi [in mathcomp_eulerian.psi_comm]
window_at_uniq [in mathcomp_eulerian.psi_descent_thms]
window_size_of_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
window_size_order_iso [in mathcomp_eulerian.psi_core]
window_trichotomy [in mathcomp_eulerian.psi_core]
window_head_extremum [in mathcomp_eulerian.psi_core]
window_at_psi_self [in mathcomp_eulerian.psi_core]
window_size_psi_self [in mathcomp_eulerian.psi_core]
window_fits_left [in mathcomp_eulerian.psi_core]
window_at_cons [in mathcomp_eulerian.psi_core]
window_size_cons [in mathcomp_eulerian.psi_core]
window_size_fuel_monotone [in mathcomp_eulerian.psi_core]
window_size_oor [in mathcomp_eulerian.psi_core]
window_size_bound [in mathcomp_eulerian.psi_core]
window_size_gt0 [in mathcomp_eulerian.psi_core]
window_size_fuel_bound [in mathcomp_eulerian.psi_core]
window_size_bound [in mathcomp_eulerian.perm_seq_bridge]
window_size_t_eq [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_gt [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_eq [in mathcomp_eulerian.psi_cdindex_tree]
window_size_t_Node_lt [in mathcomp_eulerian.psi_cdindex_tree]
window_size_last [in mathcomp_eulerian.psi_cdindex_tree]
window_size_last_fuel [in mathcomp_eulerian.psi_cdindex_tree]
witness_perm_uniq [in mathcomp_eulerian.psi_cdindex_witness]
worpitzky [in mathcomp_eulerian.eulerian]
worpitzky_binom_id [in mathcomp_eulerian.eulerian]
ws_lt_size [in mathcomp_eulerian.psi_core]
ws_core_1 [in mathcomp_eulerian.psi_cdindex_witness]
ws_bridge_right [in mathcomp_eulerian.psi_descent_v2]
ws_bridge_root [in mathcomp_eulerian.psi_descent_v2]
ws_bridge_left [in mathcomp_eulerian.psi_descent_v2]

X

xone_desc_eq [in mathcomp_eulerian.psi_descent_v2]

Constructor Index

C

C_letter [in mathcomp_eulerian.psi_cdindex_defs]

D

D_letter [in mathcomp_eulerian.psi_cdindex_defs]

E

E_letter [in mathcomp_eulerian.psi_cdindex_defs]

L

Leaf [in mathcomp_eulerian.mmtree]

N

Node [in mathcomp_eulerian.mmtree]

Inductive Index

C

cde [in mathcomp_eulerian.psi_cdindex_defs]

M

mmtree [in mathcomp_eulerian.mmtree]

Section Index

A

AltDesc [in mathcomp_eulerian.altsub]
AsPermMaxBounds [in mathcomp_eulerian.altsub]
AsPermMaxBoundsM [in mathcomp_eulerian.altsub]

B

Bridges [in mathcomp_eulerian.psi_descent_v2]

C

Cancellation [in mathcomp_eulerian.perm_compress]
CycleBasic [in mathcomp_eulerian.cycles]
CycleCountInsertAfter [in mathcomp_eulerian.stirling_fiber]

D

Descent [in mathcomp_eulerian.descent]
DescentDrop [in mathcomp_eulerian.descent]
DescentReverse [in mathcomp_eulerian.descent]
DesInsertMax [in mathcomp_eulerian.eulerian]
DropPerm [in mathcomp_eulerian.perm_compress]

E

Equidistribution [in mathcomp_eulerian.foata]
Equidistribution.FoataPerm [in mathcomp_eulerian.foata]
EulerianBasic [in mathcomp_eulerian.eulerian]
ExistenceLB [in mathcomp_eulerian.altsub]
ExtractMax [in mathcomp_eulerian.eulerian]

F

FoataBlocks [in mathcomp_eulerian.beta_omega]

H

H1 [in mathcomp_eulerian.cycles_rec]

I

InsertAfter [in mathcomp_eulerian.stirling_fiber]
InsertExtractBij [in mathcomp_eulerian.eulerian]
InsertMax [in mathcomp_eulerian.eulerian]
InterTurn [in mathcomp_eulerian.altsub]
Inversions [in mathcomp_eulerian.inversions]
InvInsertMax [in mathcomp_eulerian.qfact]
InvMajBoundsRev [in mathcomp_eulerian.inversions]

L

LiftOrd [in mathcomp_eulerian.ordinal_reindex]
LiftPerm [in mathcomp_eulerian.perm_compress]
LowerBound [in mathcomp_eulerian.altsub]

M

MajorIndex [in mathcomp_eulerian.inversions]
MaxAlternation [in mathcomp_eulerian.altsub]
MMTree [in mathcomp_eulerian.mmtree]

P

PickSeqFull [in mathcomp_eulerian.altsub]

S

SeqToPerm [in mathcomp_eulerian.perm_seq_bridge]
SignPerm [in mathcomp_eulerian.altsub]
SlotInterval [in mathcomp_eulerian.altsub]

T

TurnDefs [in mathcomp_eulerian.altsub]
TurnLemmas [in mathcomp_eulerian.altsub]

U

UnliftOrd [in mathcomp_eulerian.ordinal_reindex]
UpperBound [in mathcomp_eulerian.altsub]
UpperBoundAssembly [in mathcomp_eulerian.altsub]
UpperBoundChain [in mathcomp_eulerian.altsub]

Abbreviation Index

Q

qpow [in mathcomp_eulerian.qeul]

S

sigma [in mathcomp_eulerian.stirling_fiber]

other

σ [in mathcomp_eulerian.qfact]

Definition Index

A

all_D_transitions [in mathcomp_eulerian.psi_cdindex_support_defs]
alt_desc_set [in mathcomp_eulerian.beta_swap]
alt_321_sub [in mathcomp_eulerian.altsub]
alt_31425 [in mathcomp_eulerian.altsub]
alt_3142 [in mathcomp_eulerian.altsub]
alt_321 [in mathcomp_eulerian.altsub]
alt_312 [in mathcomp_eulerian.altsub]
alt_aux [in mathcomp_eulerian.altsub]
apply_psis [in mathcomp_eulerian.psi_cdindex_defs]
asc [in mathcomp_eulerian.descent]
as_perm [in mathcomp_eulerian.altsub]
as_perm_max [in mathcomp_eulerian.altsub]

B

beta [in mathcomp_eulerian.beta]
block_right [in mathcomp_eulerian.beta_omega]
block_left [in mathcomp_eulerian.beta_omega]

C

cde_sind [in mathcomp_eulerian.psi_cdindex_defs]
cde_rec [in mathcomp_eulerian.psi_cdindex_defs]
cde_ind [in mathcomp_eulerian.psi_cdindex_defs]
cde_rect [in mathcomp_eulerian.psi_cdindex_defs]
cde_offset [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_total_width [in mathcomp_eulerian.psi_cdindex_support_defs]
cde_width [in mathcomp_eulerian.psi_cdindex_support_defs]
char_mono [in mathcomp_eulerian.psi_cdindex_defs]
check_fact3 [in mathcomp_eulerian.psi_cdindex_core]
check_sw_5_2 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_1 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_5_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_1 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_4_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_sw_3_0 [in mathcomp_eulerian.psi_cdindex_witness]
check_strict_witness [in mathcomp_eulerian.psi_cdindex_witness]
check_phi_w_support [in mathcomp_eulerian.psi_cdindex_witness]
classify_vertex_cde [in mathcomp_eulerian.psi_cdindex_defs]
class_map [in mathcomp_eulerian.perm_seq_bridge]
coinv_set [in mathcomp_eulerian.inversions]
compl_perm [in mathcomp_eulerian.beta_swap]
count_lt [in mathcomp_eulerian.foata]
count_gt [in mathcomp_eulerian.foata]
cross_inv [in mathcomp_eulerian.foata]
cycle_count [in mathcomp_eulerian.cycles]
cyc_first_to_back [in mathcomp_eulerian.foata]
cyc_last_to_front [in mathcomp_eulerian.foata]

D

des [in mathcomp_eulerian.descent]
descent_psi_LR_swap1_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_LR_swap2_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_remove_ex [in mathcomp_eulerian.psi_descent_thms]
descent_psi_R_add_ex [in mathcomp_eulerian.psi_descent_thms]
descent_set [in mathcomp_eulerian.descent]
descent_to_bvec [in mathcomp_eulerian.perm_seq_bridge]
drop_perm [in mathcomp_eulerian.perm_compress]
drop_fun [in mathcomp_eulerian.perm_compress]
D_offsets [in mathcomp_eulerian.psi_cdindex_support_defs]

E

endpoint_next_has_left_child_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
endpoint_next_has_left_child_ex [in mathcomp_eulerian.psi_cdindex_tree]
eulerian [in mathcomp_eulerian.eulerian]
eul_pol [in mathcomp_eulerian.qeul]
exactly_one_descent_LR_ex [in mathcomp_eulerian.psi_descent_v2]
expand_cde [in mathcomp_eulerian.psi_cdindex_defs]
extract_max_perm [in mathcomp_eulerian.eulerian]
extract_max_fun [in mathcomp_eulerian.eulerian]
ex_roundtrip_compute [in mathcomp_eulerian.mmtree]
ex_roundtrip [in mathcomp_eulerian.mmtree]
ex_nontrivial [in mathcomp_eulerian.mmtree]
ex_seq [in mathcomp_eulerian.mmtree]

F

fact3_ex_213 [in mathcomp_eulerian.psi_cdindex_support]
fact3_ex_315426 [in mathcomp_eulerian.psi_cdindex_support]
find_ss [in mathcomp_eulerian.perm_seq_bridge]
flip_count [in mathcomp_eulerian.altsub]
foata [in mathcomp_eulerian.foata]
foata_perm [in mathcomp_eulerian.foata]
foata_inv [in mathcomp_eulerian.foata]
foata_inv_aux [in mathcomp_eulerian.foata]
foata_step_undo [in mathcomp_eulerian.foata]
foata_step [in mathcomp_eulerian.foata]

H

has_transition [in mathcomp_eulerian.psi_cdindex_support_defs]
has_left_child_t [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_psi_ex [in mathcomp_eulerian.psi_cdindex_tree]
has_left_child_true [in mathcomp_eulerian.psi_descent_v2]
has_left_child_false [in mathcomp_eulerian.psi_descent_v2]
has_left_child [in mathcomp_eulerian.psi_descent_v2]
has_left_child_fuel [in mathcomp_eulerian.psi_descent_v2]

I

insert_max_perm [in mathcomp_eulerian.eulerian]
insert_max_fun [in mathcomp_eulerian.eulerian]
insert_after [in mathcomp_eulerian.stirling_fiber]
insert_after_fun [in mathcomp_eulerian.stirling_fiber]
internal_vertices [in mathcomp_eulerian.psi_cdindex_defs]
inv [in mathcomp_eulerian.inversions]
inv_set [in mathcomp_eulerian.inversions]
inv_seq [in mathcomp_eulerian.foata]
is_inv [in mathcomp_eulerian.inversions]
is_internal [in mathcomp_eulerian.psi_cdindex_defs]
is_desc_seq [in mathcomp_eulerian.foata]
is_descent [in mathcomp_eulerian.descent]
is_alt_bool [in mathcomp_eulerian.altsub]
is_alt_bool_aux [in mathcomp_eulerian.altsub]
is_alt [in mathcomp_eulerian.altsub]
is_turn [in mathcomp_eulerian.altsub]
is_internal_t [in mathcomp_eulerian.psi_cdindex_tree]
is_D_letter [in mathcomp_eulerian.psi_cdindex_witness]
is_descent_seq_ex [in mathcomp_eulerian.psi_descent_v2]
is_descent_seq [in mathcomp_eulerian.psi_descent_v2]

L

left_ok [in mathcomp_eulerian.beta_omega]
leq_seqb [in mathcomp_eulerian.psi_cdindex_defs]
lift_perm [in mathcomp_eulerian.perm_compress]
lift_fun [in mathcomp_eulerian.perm_compress]
LR_pred_is_endpoint_ex3 [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
LR_pred_is_endpoint_ex [in mathcomp_eulerian.psi_cdindex_tree]

M

maj [in mathcomp_eulerian.inversions]
maj_seq [in mathcomp_eulerian.foata]
max_pos [in mathcomp_eulerian.psi_core]
min_pos [in mathcomp_eulerian.mmtree]
mmtree_shape [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_shape_fuel [in mathcomp_eulerian.psi_cdindex_tree_shape]
mmtree_of_seq [in mathcomp_eulerian.mmtree]
mmtree_of_seq_fuel [in mathcomp_eulerian.mmtree]
mmtree_to_seq [in mathcomp_eulerian.mmtree]
mmtree_sind [in mathcomp_eulerian.mmtree]
mmtree_rec [in mathcomp_eulerian.mmtree]
mmtree_ind [in mathcomp_eulerian.mmtree]
mmtree_rect [in mathcomp_eulerian.mmtree]
mmtree_of_seq_mm [in mathcomp_eulerian.psi_core]
mmtree_of_seq_mm_fuel [in mathcomp_eulerian.psi_core]
mm_pos [in mathcomp_eulerian.psi_core]

O

omega_set [in mathcomp_eulerian.beta_omega]
omega_seq_local [in mathcomp_eulerian.beta_bridge]
omega_seq [in mathcomp_eulerian.psi_cdindex_witness]

P

perm_seq [in mathcomp_eulerian.altsub]
perm_to_seq [in mathcomp_eulerian.perm_seq_bridge]
phi_w [in mathcomp_eulerian.psi_cdindex_defs]
phi_w_support_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
phi'_w [in mathcomp_eulerian.psi_cdindex_defs]
pick_seq [in mathcomp_eulerian.altsub]
post_window_extremum_ex [in mathcomp_eulerian.psi_descent_v2]
pos_seq [in mathcomp_eulerian.altsub]
powerset_internal [in mathcomp_eulerian.psi_cdindex_defs]
pre_window_gt_min_ex [in mathcomp_eulerian.psi_descent_v2]
psi [in mathcomp_eulerian.psi_core]
psi_comm_nontrivial [in mathcomp_eulerian.psi_comm]
psi_comm_ex [in mathcomp_eulerian.psi_comm]
psi_comm_nested_ex [in mathcomp_eulerian.psi_comm]
psi_comm_disjoint_ex [in mathcomp_eulerian.psi_comm]
psi_involutive_ex [in mathcomp_eulerian.psi_core]
psi_nontrivial [in mathcomp_eulerian.psi_core]

Q

q_fact [in mathcomp_eulerian.qfact]
q_int [in mathcomp_eulerian.qfact]
q_eul_pol [in mathcomp_eulerian.qeul]
q1_subst [in mathcomp_eulerian.qeul]

R

rank_shift_seq [in mathcomp_eulerian.psi_core]
rank_shift_interior_order_ex [in mathcomp_eulerian.psi_descent_v2]
rev_perm [in mathcomp_eulerian.descent]
rev_perm_ord [in mathcomp_eulerian.descent]
right_ok [in mathcomp_eulerian.beta_omega]

S

seq_to_perm [in mathcomp_eulerian.perm_seq_bridge]
seq_to_fun [in mathcomp_eulerian.perm_seq_bridge]
set_to_seq [in mathcomp_eulerian.beta_bridge]
set_is_alt [in mathcomp_eulerian.beta_swap]
sign_seq [in mathcomp_eulerian.altsub]
slot_iv [in mathcomp_eulerian.altsub]
split_blocks_inv [in mathcomp_eulerian.foata]
split_blocks_inv_aux [in mathcomp_eulerian.foata]
split_blocks [in mathcomp_eulerian.foata]
split_blocks_aux [in mathcomp_eulerian.foata]
stirling_c [in mathcomp_eulerian.cycles]
strict_witness_ex3 [in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex2 [in mathcomp_eulerian.psi_cdindex_witness]
strict_witness_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
sym_diff [in mathcomp_eulerian.beta_omega]
S_w_seq_ex4 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex3 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex2 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq_ex1 [in mathcomp_eulerian.psi_cdindex_witness]
S_w_seq [in mathcomp_eulerian.psi_cdindex_witness]

T

tcs_12345 [in mathcomp_eulerian.altsub]
tcs_321 [in mathcomp_eulerian.altsub]
tcs_3142 [in mathcomp_eulerian.altsub]
tcs_312 [in mathcomp_eulerian.altsub]
toggle_at [in mathcomp_eulerian.beta_omega]
tree_props [in mathcomp_eulerian.psi_descent_v2]
turn_witness [in mathcomp_eulerian.altsub]
turn_inj [in mathcomp_eulerian.altsub]
turn_iv [in mathcomp_eulerian.altsub]
turn_count_seq [in mathcomp_eulerian.altsub]
turn_count [in mathcomp_eulerian.altsub]

U

uniq_adj [in mathcomp_eulerian.altsub]

V

valid_mm [in mathcomp_eulerian.psi_descent_v2]

W

wf_block [in mathcomp_eulerian.foata]
window_size_psi_ancestor_ex [in mathcomp_eulerian.psi_comm]
window_trichotomy_ex [in mathcomp_eulerian.psi_core]
window_at [in mathcomp_eulerian.psi_core]
window_size [in mathcomp_eulerian.psi_core]
window_size_fuel [in mathcomp_eulerian.psi_core]
window_size_t [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex3 [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex2 [in mathcomp_eulerian.psi_cdindex_tree]
window_size_psi_ex1 [in mathcomp_eulerian.psi_cdindex_tree]
witness_perm [in mathcomp_eulerian.psi_cdindex_witness]

Global Index

J

K

Y

Z

_

(1044 entries)

Variable Index

G

J

K

N

O

Q

R

V

W

X

Y

Z

_

other

(60 entries)

Library Index

G

H

J

K

L

N

R

T

U

V

W

X

Y

Z

_

other

(31 entries)

Lemma Index

J

K

Y

Z

_

other

(704 entries)

Constructor Index

A

B

F

G

H

I

J

K

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Section Index

G

J

K

N

O

Q

R

V

W

X

Y

Z

_

other

(42 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

R

T

U

V

W

X

Y

Z

_

(3 entries)

Definition Index

G

J

K

N

X

Y

Z

_

other

(197 entries)

This page has been generated by coqdoc