_CoqProject

-R . mathcomp_eulerian
-R fps mathcomp_fps

-arg -w -arg -deprecated-library-file
-arg -w -arg -notation-overridden

# mathcomp_fps: self-contained formal power series sub-library
# (depends on mathcomp + mathcomp-classical only; see fps/README.md
# and docs/plans/FPS_PLAN.md).
fps/fps.v
fps/fps_deriv.v
fps/fps_egf.v
fps/fps_trig.v
fps/fps_ode.v
fps/fps_ogf.v
fps/fps_comp.v
fps/fps_explog.v

mmtree.v
psi_core.v
psi_comm.v
# §1.4 closure first; perm_seq_basics is the psi-free perm <-> seq bridge.
ordinal_reindex.v
perm_compress.v
descent.v
eulerian.v
beta.v
beta_omega.v
beta_bridge.v
perm_seq_basics.v
# psi_descent_v2 imports perm_seq_basics for [is_descent_seq].
psi_descent_v2.v
psi_descent_thms.v
# Compatibility wrapper for psi_descent_v2.v + psi_descent_thms.v.
psi_descent.v
psi_cdindex_defs.v
psi_cdindex_tree_shape.v
psi_cdindex_tree_hlc.v
psi_cdindex_tree.v
psi_cdindex_core.v
psi_cdindex_witness.v
psi_cdindex_support_defs.v
psi_cdindex_support.v
# perm_seq_bridge holds the cd-index half (uses psi_*); see
# docs/plans/CD_INDEX_SEPARATION_PLAN.md.
perm_seq_bridge.v
beta_swap.v
# Worpitzky identity (axiom-free, Stanley §1.4); needs eulerian + qeul.
worpitzky.v
# Gaussian binomials (axiom-free); q-staircase lives in carlitz.v.
qbin.v
# q-Eulerian (maj,des) insertion recurrence (axiom-free... 1 stub WIP).
qeul_rec.v
# Carlitz q-Worpitzky identity (axiom-free combinatorial core).
qworpitzky.v
# reflection.v: André's reflection method (Stanley §1.6.4); euler_rec.
# The former named admit (sum_set_is_alt_eq_andre_sum) is now fully
# proved — 0 admits, 0 axioms.
reflection.v
# Stanley Prop 1.6.1: bridge between reflection.v and mathcomp_fps.
stanley_egf.v
# Stanley §1.4 OGF (Worpitzky packaged as generating functions).
stanley_ogf.v
# Stirling-cycle EGF demo (phase 3, demo #2).
stirling_egf.v
# Carlitz denominator: the q-staircase (phase 4, part 1).
carlitz.v
cycles.v
cycles_rec.v
stirling_fiber.v
inversions.v
foata.v
qfact.v
qeul.v
altsub.v