O (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
O (Lemmas)
oACE [prf, in mathcomp.boot.bigop]odd_2'nat [prf, in mathcomp.boot.prime]
odd_double [prf, in mathcomp.boot.ssrnat]
odd_double_half [prf, in mathcomp.boot.ssrnat]
odd_geq [prf, in mathcomp.boot.ssrnat]
odd_gt0 [prf, in mathcomp.boot.ssrnat]
odd_gt2 [prf, in mathcomp.boot.ssrnat]
odd_halfK [prf, in mathcomp.boot.ssrnat]
odd_lift_perm [prf, in mathcomp.finite_group.perm]
odd_ltn [prf, in mathcomp.boot.ssrnat]
odd_mod [prf, in mathcomp.boot.div]
odd_mul_tperm [prf, in mathcomp.finite_group.perm]
odd_not_extremal2 [prf, in mathcomp.solvable.extremal]
odd_perm1 [prf, in mathcomp.finite_group.perm]
odd_perm_prod [prf, in mathcomp.finite_group.perm]
odd_permJ [prf, in mathcomp.finite_group.perm]
odd_permM [prf, in mathcomp.finite_group.perm]
odd_permV [prf, in mathcomp.finite_group.perm]
odd_pgroup_odd [prf, in mathcomp.solvable.pgroup]
odd_pgroup_rank1_cyclic [prf, in mathcomp.solvable.extremal]
odd_poly_is_linear [prf, in mathcomp.algebra.poly]
odd_polyC [prf, in mathcomp.algebra.poly]
odd_polyD [prf, in mathcomp.algebra.poly]
odd_polyE [prf, in mathcomp.algebra.poly]
odd_polyMX [prf, in mathcomp.algebra.poly]
odd_polyZ [prf, in mathcomp.algebra.poly]
odd_prime_gt2 [prf, in mathcomp.boot.prime]
odd_tperm [prf, in mathcomp.finite_group.perm]
odd_uphalfK [prf, in mathcomp.boot.ssrnat]
oddB [prf, in mathcomp.boot.ssrnat]
oddb [prf, in mathcomp.boot.ssrnat]
oddD [prf, in mathcomp.boot.ssrnat]
oddM [prf, in mathcomp.boot.ssrnat]
oddN [prf, in mathcomp.boot.ssrnat]
oddS [prf, in mathcomp.boot.ssrnat]
oddSg [prf, in mathcomp.solvable.pgroup]
oddX [prf, in mathcomp.boot.ssrnat]
odflt_onth [prf, in mathcomp.boot.seq]
of_family_tagged_with_bij [prf, in mathcomp.boot.finfun]
of_family_tagged_withK [prf, in mathcomp.boot.finfun]
of_irrK [prf, in mathcomp.group_representation.vcharacter]
Ohm0 [prf, in mathcomp.solvable.abelian]
Ohm1 [prf, in mathcomp.solvable.abelian]
Ohm1_abelem [prf, in mathcomp.solvable.abelian]
Ohm1_cent_max [prf, in mathcomp.solvable.abelian]
Ohm1_cent_max_normal_abelem [prf, in mathcomp.solvable.maximal]
Ohm1_cyclic_pgroup_prime [prf, in mathcomp.solvable.abelian]
Ohm1_eq1 [prf, in mathcomp.solvable.abelian]
Ohm1_extraspecial_odd [prf, in mathcomp.solvable.extraspecial]
Ohm1_homocyclicP [prf, in mathcomp.solvable.abelian]
Ohm1_id [prf, in mathcomp.solvable.abelian]
Ohm1_stab_Ohm1_SCN_series [prf, in mathcomp.solvable.maximal]
Ohm1Eexponent [prf, in mathcomp.solvable.abelian]
Ohm1Eprime [prf, in mathcomp.solvable.abelian]
Ohm_char [prf, in mathcomp.solvable.abelian]
Ohm_cont [prf, in mathcomp.solvable.abelian]
Ohm_dprod [prf, in mathcomp.solvable.abelian]
Ohm_id [prf, in mathcomp.solvable.abelian]
Ohm_leq [prf, in mathcomp.solvable.abelian]
Ohm_Mho_homocyclic [prf, in mathcomp.solvable.abelian]
Ohm_normal [prf, in mathcomp.solvable.abelian]
Ohm_p_cycle [prf, in mathcomp.solvable.abelian]
Ohm_sub [prf, in mathcomp.solvable.abelian]
OhmE [prf, in mathcomp.solvable.abelian]
OhmEabelian [prf, in mathcomp.solvable.abelian]
OhmJ [prf, in mathcomp.solvable.abelian]
OhmPredP [prf, in mathcomp.solvable.abelian]
OhmS [prf, in mathcomp.solvable.abelian]
olaw1x [prf, in mathcomp.boot.bigop]
olawss [prf, in mathcomp.boot.bigop]
olawx1 [prf, in mathcomp.boot.bigop]
omap_id [prf, in mathcomp.boot.ssrfun]
omap_unset1K [prf, in mathcomp.boot.finset]
omapK [prf, in mathcomp.boot.ssrfun]
on_card_preimset [prf, in mathcomp.boot.finset]
one_fun_gmulf1 [prf, in mathcomp.boot.monoid]
one_fun_gmulfM [prf, in mathcomp.boot.monoid]
oneg_ffun [prf, in mathcomp.finite_group.gproduct]
onth0n [prf, in mathcomp.boot.seq]
onth1P [prf, in mathcomp.boot.seq]
onth_cat [prf, in mathcomp.boot.seq]
onth_default [prf, in mathcomp.boot.seq]
onth_inj [prf, in mathcomp.boot.seq]
onth_map [prf, in mathcomp.boot.seq]
onth_nseq [prf, in mathcomp.boot.seq]
onth_nth [prf, in mathcomp.boot.seq]
onthE [prf, in mathcomp.boot.seq]
onthNE [prf, in mathcomp.boot.seq]
onthP [prf, in mathcomp.boot.seq]
onthPn [prf, in mathcomp.boot.seq]
onthTE [prf, in mathcomp.boot.seq]
op_Wedderburn_id_pchar [prf, in mathcomp.group_representation.mxrepresentation]
opair_of_sumK [prf, in mathcomp.boot.choice]
opp_block_mx [prf, in mathcomp.algebra.matrix]
opp_col_mx [prf, in mathcomp.algebra.matrix]
opp_isometry [prf, in mathcomp.group_representation.classfun]
opp_lfunE [prf, in mathcomp.algebra.vector]
opp_poly_key [prf, in mathcomp.algebra.poly]
opp_row_mx [prf, in mathcomp.algebra.matrix]
oppmx_key [prf, in mathcomp.algebra.matrix]
oppq_frac [prf, in mathcomp.algebra.rat]
opt_eqP [prf, in mathcomp.boot.eqtype]
option_enumP [prf, in mathcomp.boot.fintype]
orbit1P [prf, in mathcomp.finite_group.action]
orbit_act [prf, in mathcomp.finite_group.action]
orbit_act_in [prf, in mathcomp.finite_group.action]
orbit_actr [prf, in mathcomp.finite_group.action]
orbit_actr_in [prf, in mathcomp.finite_group.action]
orbit_conjsg [prf, in mathcomp.finite_group.action]
orbit_conjsg_in [prf, in mathcomp.finite_group.action]
orbit_eq_mem [prf, in mathcomp.finite_group.action]
orbit_eqP [prf, in mathcomp.finite_group.action]
orbit_id [prf, in mathcomp.boot.fingraph]
orbit_in_eqP [prf, in mathcomp.finite_group.action]
orbit_in_sym [prf, in mathcomp.finite_group.action]
orbit_in_trans [prf, in mathcomp.finite_group.action]
orbit_in_transl [prf, in mathcomp.finite_group.action]
orbit_inv [prf, in mathcomp.finite_group.action]
orbit_inv_in [prf, in mathcomp.finite_group.action]
orbit_lcoset [prf, in mathcomp.finite_group.action]
orbit_lcoset_in [prf, in mathcomp.finite_group.action]
orbit_morphim_actperm [prf, in mathcomp.finite_group.action]
orbit_partition [prf, in mathcomp.finite_group.action]
orbit_rcoset [prf, in mathcomp.finite_group.action]
orbit_rcoset_in [prf, in mathcomp.finite_group.action]
orbit_refl [prf, in mathcomp.finite_group.action]
orbit_rot_cycle [prf, in mathcomp.boot.fingraph]
orbit_stabilizer [prf, in mathcomp.finite_group.action]
orbit_sym [prf, in mathcomp.finite_group.action]
orbit_trans [prf, in mathcomp.finite_group.action]
orbit_transl [prf, in mathcomp.finite_group.action]
orbit_transversalP [prf, in mathcomp.finite_group.action]
orbit_uniq [prf, in mathcomp.boot.fingraph]
orbitE [prf, in mathcomp.finite_group.action]
orbitE [prf, in mathcomp.boot.fingraph]
orbitJ [prf, in mathcomp.finite_group.action]
orbitJs [prf, in mathcomp.finite_group.action]
orbitP [prf, in mathcomp.finite_group.action]
orbitPcycle [prf, in mathcomp.boot.fingraph]
orbitR [prf, in mathcomp.finite_group.action]
orbitRs [prf, in mathcomp.finite_group.action]
ord1 [prf, in mathcomp.boot.nmodule]
ord1 [prf, in mathcomp.boot.fintype]
ord_enum4 [prf, in mathcomp.solvable.burnside_app]
ord_enum_uniq [prf, in mathcomp.boot.fintype]
ord_inj [prf, in mathcomp.boot.fintype]
ord_pred_bij [prf, in mathcomp.boot.fintype]
ord_pred_inj [prf, in mathcomp.boot.fintype]
ord_predK [prf, in mathcomp.boot.fintype]
ord_prod_nil [prf, in mathcomp.algebra.tensor]
Order.BDistrLatticeTheory.disjoint_lexUl [prf, in mathcomp.order.order]
Order.BDistrLatticeTheory.disjoint_lexUr [prf, in mathcomp.order.order]
Order.BDistrLatticeTheory.joins_disjoint [prf, in mathcomp.order.order]
Order.BDistrLatticeTheory.leU2E [prf, in mathcomp.order.order]
Order.BDistrLatticeTheory.leU2l_le [prf, in mathcomp.order.order]
Order.BDistrLatticeTheory.leU2r_le [prf, in mathcomp.order.order]
Order.BJoinTheory.join0x [prf, in mathcomp.order.order]
Order.BJoinTheory.join_eq0 [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_le [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_min [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_min_seq [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_seq [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_setU [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_sup [prf, in mathcomp.order.order]
Order.BJoinTheory.joins_sup_seq [prf, in mathcomp.order.order]
Order.BJoinTheory.joinsP [prf, in mathcomp.order.order]
Order.BJoinTheory.joinsP_seq [prf, in mathcomp.order.order]
Order.BJoinTheory.joinx0 [prf, in mathcomp.order.order]
Order.BJoinTheory.le_joins [prf, in mathcomp.order.order]
Order.BLatticeMorphismTheory.comp_is_bottom_morphism [prf, in mathcomp.order.order]
Order.BLatticeMorphismTheory.idfun_is_bottom_morphism [prf, in mathcomp.order.order]
Order.BLatticeMorphismTheory.omorph0 [prf, in mathcomp.order.order]
Order.BMeetTheory.meet0x [prf, in mathcomp.order.order]
Order.BMeetTheory.meetx0 [prf, in mathcomp.order.order]
Order.BoolOrder.andbE [prf, in mathcomp.order.order]
Order.BoolOrder.andEbool [prf, in mathcomp.order.order]
Order.BoolOrder.andKb [prf, in mathcomp.order.order]
Order.BoolOrder.anti [prf, in mathcomp.order.order]
Order.BoolOrder.bool_display [prf, in mathcomp.order.preorder]
Order.BoolOrder.complEbool [prf, in mathcomp.order.order]
Order.BoolOrder.leEbool [prf, in mathcomp.order.preorder]
Order.BoolOrder.leEmeet [prf, in mathcomp.order.order]
Order.BoolOrder.ltEbool [prf, in mathcomp.order.preorder]
Order.BoolOrder.ltn_def [prf, in mathcomp.order.preorder]
Order.BoolOrder.orbE [prf, in mathcomp.order.order]
Order.BoolOrder.orEbool [prf, in mathcomp.order.order]
Order.BoolOrder.orKb [prf, in mathcomp.order.order]
Order.BoolOrder.subEbool [prf, in mathcomp.order.order]
Order.BPOrderTheory.lex0 [prf, in mathcomp.order.order]
Order.BPOrderTheory.lt0x [prf, in mathcomp.order.order]
Order.BPOrderTheory.posxP [prf, in mathcomp.order.order]
Order.BPreorderTheory.le0x [prf, in mathcomp.order.preorder]
Order.BPreorderTheory.ltx0 [prf, in mathcomp.order.preorder]
Order.Builders_111.joinxx [prf, in mathcomp.order.order]
Order.Builders_111.leEjoin [prf, in mathcomp.order.order]
Order.Builders_111.leUx [prf, in mathcomp.order.order]
Order.Builders_111.lexI [prf, in mathcomp.order.order]
Order.Builders_111.meetxx [prf, in mathcomp.order.order]
Order.Builders_130.le_anti [prf, in mathcomp.order.order]
Order.Builders_130.le_refl [prf, in mathcomp.order.order]
Order.Builders_130.le_trans [prf, in mathcomp.order.order]
Order.Builders_130.lt_le_def [prf, in mathcomp.order.order]
Order.Builders_141.diffErcompl [prf, in mathcomp.order.order]
Order.Builders_141.rcomplPjoin [prf, in mathcomp.order.order]
Order.Builders_141.rcomplPmeet [prf, in mathcomp.order.order]
Order.Builders_148.codiffErcompl [prf, in mathcomp.order.order]
Order.Builders_148.rcomplPjoin [prf, in mathcomp.order.order]
Order.Builders_148.rcomplPmeet [prf, in mathcomp.order.order]
Order.Builders_155.complEcodiff [prf, in mathcomp.order.order]
Order.Builders_162.complEdiff [prf, in mathcomp.order.order]
Order.Builders_169.codiffErcompl [prf, in mathcomp.order.order]
Order.Builders_169.complEcodiff [prf, in mathcomp.order.order]
Order.Builders_169.complEdiff [prf, in mathcomp.order.order]
Order.Builders_169.diffKI [prf, in mathcomp.order.order]
Order.Builders_169.joinIB [prf, in mathcomp.order.order]
Order.Builders_179.meetUl [prf, in mathcomp.order.order]
Order.Builders_186.joinA [prf, in mathcomp.order.order]
Order.Builders_186.joinC [prf, in mathcomp.order.order]
Order.Builders_186.joinKI [prf, in mathcomp.order.order]
Order.Builders_186.leEmeet [prf, in mathcomp.order.order]
Order.Builders_186.leP [prf, in mathcomp.order.order]
Order.Builders_186.ltgtP [prf, in mathcomp.order.order]
Order.Builders_186.meetA [prf, in mathcomp.order.order]
Order.Builders_186.meetC [prf, in mathcomp.order.order]
Order.Builders_186.meetKU [prf, in mathcomp.order.order]
Order.Builders_195.joinA [prf, in mathcomp.order.order]
Order.Builders_195.joinC [prf, in mathcomp.order.order]
Order.Builders_195.joinE [prf, in mathcomp.order.order]
Order.Builders_195.joinKI [prf, in mathcomp.order.order]
Order.Builders_195.le_def [prf, in mathcomp.order.order]
Order.Builders_195.le_refl [prf, in mathcomp.order.order]
Order.Builders_195.lt_le_def [prf, in mathcomp.order.order]
Order.Builders_195.meetA [prf, in mathcomp.order.order]
Order.Builders_195.meetC [prf, in mathcomp.order.order]
Order.Builders_195.meetE [prf, in mathcomp.order.order]
Order.Builders_195.meetKU [prf, in mathcomp.order.order]
Order.Builders_195.meetUl [prf, in mathcomp.order.order]
Order.Builders_195.meetxx [prf, in mathcomp.order.order]
Order.Builders_226.join_def_le [prf, in mathcomp.order.order]
Order.Builders_226.le_anti [prf, in mathcomp.order.order]
Order.Builders_226.le_total [prf, in mathcomp.order.order]
Order.Builders_226.le_trans [prf, in mathcomp.order.order]
Order.Builders_226.lt_def [prf, in mathcomp.order.order]
Order.Builders_226.meet_def_le [prf, in mathcomp.order.order]
Order.Builders_236.totalT [prf, in mathcomp.order.order]
Order.Builders_275.isobottom [prf, in mathcomp.order.order]
Order.Builders_280.isotop [prf, in mathcomp.order.order]
Order.Builders_285.joinA [prf, in mathcomp.order.order]
Order.Builders_285.joinC [prf, in mathcomp.order.order]
Order.Builders_285.joinKI [prf, in mathcomp.order.order]
Order.Builders_285.meet_eql [prf, in mathcomp.order.order]
Order.Builders_285.meetA [prf, in mathcomp.order.order]
Order.Builders_285.meetC [prf, in mathcomp.order.order]
Order.Builders_285.meetKI [prf, in mathcomp.order.order]
Order.Builders_291.meetUl [prf, in mathcomp.order.order]
Order.Builders_361.joinUKI [prf, in mathcomp.order.order]
Order.Builders_361.valI [prf, in mathcomp.order.order]
Order.Builders_361.valU [prf, in mathcomp.order.order]
Order.Builders_391.le0x [prf, in mathcomp.order.order]
Order.Builders_391.val0 [prf, in mathcomp.order.order]
Order.Builders_415.lex1 [prf, in mathcomp.order.order]
Order.Builders_415.val1 [prf, in mathcomp.order.order]
Order.Builders_464.totalU [prf, in mathcomp.order.order]
Order.Builders_470.opredI [prf, in mathcomp.order.order]
Order.Builders_470.opredU [prf, in mathcomp.order.order]
Order.Builders_67.valD [prf, in mathcomp.order.preorder]
Order.Builders_94.lexI [prf, in mathcomp.order.order]
Order.Builders_94.meetxx [prf, in mathcomp.order.order]
Order.Builders_99.joinxx [prf, in mathcomp.order.order]
Order.Builders_99.leUx [prf, in mathcomp.order.order]
Order.CancelPartial.anti [prf, in mathcomp.order.order]
Order.CancelPartial.lt_def [prf, in mathcomp.order.order]
Order.cardE [prf, in mathcomp.order.preorder]
Order.cardT [prf, in mathcomp.order.preorder]
Order.CBDistrLatticeTheory.diff0x [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diff_eq0 [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffBx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffErcompl [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffIK [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffIx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffKI [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffKU [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffUK [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffUx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffx0 [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffxB [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffxI [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffxU [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.diffxx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.disj_diffl [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.disj_diffr [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.disj_le [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.disj_leC [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.eq_diff [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinBI [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinBIC [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinBK [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinBKC [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinBx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinIB [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinIBC [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.joinxB [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leB2 [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBKU [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBl [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBLR [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBr [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBRL [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBUK [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.leBx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.lt0B [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.meet_eq0E_diff [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.meetBI [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.meetBx [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.meetIB [prf, in mathcomp.order.order]
Order.CBDistrLatticeTheory.meetxB [prf, in mathcomp.order.order]
Order.CDistrLatticeTheory.rcomplKI [prf, in mathcomp.order.order]
Order.CDistrLatticeTheory.rcomplKU [prf, in mathcomp.order.order]
Order.CDistrLatticeTheory.rcomplPjoin [prf, in mathcomp.order.order]
Order.CDistrLatticeTheory.rcomplPmeet [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.compl0 [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.compl1 [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.compl_inj [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.compl_joins [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.compl_meets [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complB [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complEcodiff [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complEdiff [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complErcompl [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complI [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complK [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.complU [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.diff1x [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.diffE [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.disj_leC [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.joinCx [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.joinxC [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.leBC [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.leC [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.leCx [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.lexC [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.meetCx [prf, in mathcomp.order.order]
Order.CTBDistrLatticeTheory.meetxC [prf, in mathcomp.order.order]
Order.CTDistrLatticeTheory.codiffErcompl [prf, in mathcomp.order.order]
Order.DistrLatticeTheory.joinIl [prf, in mathcomp.order.order]
Order.DistrLatticeTheory.joinIr [prf, in mathcomp.order.order]
Order.DistrLatticeTheory.meetUl [prf, in mathcomp.order.order]
Order.DistrLatticeTheory.meetUr [prf, in mathcomp.order.order]
Order.DualOrder.joinEdual [prf, in mathcomp.order.order]
Order.DualOrder.meetEdual [prf, in mathcomp.order.order]
Order.DualPreorder.botEdual [prf, in mathcomp.order.preorder]
Order.DualPreorder.leEdual [prf, in mathcomp.order.preorder]
Order.DualPreorder.ltEdual [prf, in mathcomp.order.preorder]
Order.DualPreorder.topEdual [prf, in mathcomp.order.preorder]
Order.dvd_display [prf, in mathcomp.order.preorder]
Order.enum0 [prf, in mathcomp.order.preorder]
Order.enum1 [prf, in mathcomp.order.preorder]
Order.enum_ord [prf, in mathcomp.order.preorder]
Order.enum_set0 [prf, in mathcomp.order.preorder]
Order.enum_set1 [prf, in mathcomp.order.preorder]
Order.enum_setT [prf, in mathcomp.order.preorder]
Order.enum_uniq [prf, in mathcomp.order.preorder]
Order.enumT [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_rank_bij [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_rank_in_inj [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_rank_inj [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_rankK [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_rankK_in [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_val_bij [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_val_bij_in [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_val_inj [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_val_nth [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_valK [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_valK_in [prf, in mathcomp.order.preorder]
Order.EnumVal.enum_valP [prf, in mathcomp.order.preorder]
Order.EnumVal.eq_enum_rank_in [prf, in mathcomp.order.preorder]
Order.EnumVal.le_enum_rank [prf, in mathcomp.order.order]
Order.EnumVal.le_enum_rank_in [prf, in mathcomp.order.order]
Order.EnumVal.le_enum_val [prf, in mathcomp.order.order]
Order.EnumVal.nth_enum_rank [prf, in mathcomp.order.preorder]
Order.EnumVal.nth_enum_rank_in [prf, in mathcomp.order.preorder]
Order.eq_cardT [prf, in mathcomp.order.preorder]
Order.eq_enum [prf, in mathcomp.order.preorder]
Order.index_enum_ord [prf, in mathcomp.order.preorder]
Order.JoinTheory.eq_joinl [prf, in mathcomp.order.order]
Order.JoinTheory.eq_joinr [prf, in mathcomp.order.order]
Order.JoinTheory.join_idPl [prf, in mathcomp.order.order]
Order.JoinTheory.join_idPr [prf, in mathcomp.order.order]
Order.JoinTheory.join_l [prf, in mathcomp.order.order]
Order.JoinTheory.join_r [prf, in mathcomp.order.order]
Order.JoinTheory.joinA [prf, in mathcomp.order.order]
Order.JoinTheory.joinAC [prf, in mathcomp.order.order]
Order.JoinTheory.joinACA [prf, in mathcomp.order.order]
Order.JoinTheory.joinC [prf, in mathcomp.order.order]
Order.JoinTheory.joinCA [prf, in mathcomp.order.order]
Order.JoinTheory.joinKU [prf, in mathcomp.order.order]
Order.JoinTheory.joinKUC [prf, in mathcomp.order.order]
Order.JoinTheory.joinUK [prf, in mathcomp.order.order]
Order.JoinTheory.joinUKC [prf, in mathcomp.order.order]
Order.JoinTheory.joinxx [prf, in mathcomp.order.order]
Order.JoinTheory.leEjoin [prf, in mathcomp.order.order]
Order.JoinTheory.leU2 [prf, in mathcomp.order.order]
Order.JoinTheory.leUidl [prf, in mathcomp.order.order]
Order.JoinTheory.leUidr [prf, in mathcomp.order.order]
Order.JoinTheory.leUl [prf, in mathcomp.order.order]
Order.JoinTheory.leUr [prf, in mathcomp.order.order]
Order.JoinTheory.leUx [prf, in mathcomp.order.order]
Order.JoinTheory.lexU2 [prf, in mathcomp.order.order]
Order.JoinTheory.lexUl [prf, in mathcomp.order.order]
Order.JoinTheory.lexUr [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.comp_is_join_morphism [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.comp_is_meet_morphism [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.idfun_is_join_morphism [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.idfun_is_meet_morphism [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.omorphI [prf, in mathcomp.order.order]
Order.LatticeMorphismTheory.omorphU [prf, in mathcomp.order.order]
Order.LatticePred.opred0 [prf, in mathcomp.order.order]
Order.LatticePred.opred1 [prf, in mathcomp.order.order]
Order.LatticePred.opred_joins [prf, in mathcomp.order.order]
Order.LatticePred.opred_meets [prf, in mathcomp.order.order]
Order.LatticePred.opredI [prf, in mathcomp.order.order]
Order.LatticePred.opredU [prf, in mathcomp.order.order]
Order.LatticeTheory.joinIK [prf, in mathcomp.order.order]
Order.LatticeTheory.joinIKC [prf, in mathcomp.order.order]
Order.LatticeTheory.joinKI [prf, in mathcomp.order.order]
Order.LatticeTheory.joinKIC [prf, in mathcomp.order.order]
Order.LatticeTheory.lcomparable_leP [prf, in mathcomp.order.order]
Order.LatticeTheory.lcomparable_ltgtP [prf, in mathcomp.order.order]
Order.LatticeTheory.lcomparable_ltP [prf, in mathcomp.order.order]
Order.LatticeTheory.lcomparableP [prf, in mathcomp.order.order]
Order.LatticeTheory.meetKU [prf, in mathcomp.order.order]
Order.LatticeTheory.meetKUC [prf, in mathcomp.order.order]
Order.LatticeTheory.meetUK [prf, in mathcomp.order.order]
Order.LatticeTheory.meetUKC [prf, in mathcomp.order.order]
Order.lexi_display [prf, in mathcomp.order.preorder]
Order.MeetTheory.eq_meetl [prf, in mathcomp.order.order]
Order.MeetTheory.eq_meetr [prf, in mathcomp.order.order]
Order.MeetTheory.leEmeet [prf, in mathcomp.order.order]
Order.MeetTheory.leI2 [prf, in mathcomp.order.order]
Order.MeetTheory.leIidl [prf, in mathcomp.order.order]
Order.MeetTheory.leIidr [prf, in mathcomp.order.order]
Order.MeetTheory.leIl [prf, in mathcomp.order.order]
Order.MeetTheory.leIr [prf, in mathcomp.order.order]
Order.MeetTheory.leIx2 [prf, in mathcomp.order.order]
Order.MeetTheory.leIxl [prf, in mathcomp.order.order]
Order.MeetTheory.leIxr [prf, in mathcomp.order.order]
Order.MeetTheory.lexI [prf, in mathcomp.order.order]
Order.MeetTheory.meet_idPl [prf, in mathcomp.order.order]
Order.MeetTheory.meet_idPr [prf, in mathcomp.order.order]
Order.MeetTheory.meet_l [prf, in mathcomp.order.order]
Order.MeetTheory.meet_r [prf, in mathcomp.order.order]
Order.MeetTheory.meetA [prf, in mathcomp.order.order]
Order.MeetTheory.meetAC [prf, in mathcomp.order.order]
Order.MeetTheory.meetACA [prf, in mathcomp.order.order]
Order.MeetTheory.meetC [prf, in mathcomp.order.order]
Order.MeetTheory.meetCA [prf, in mathcomp.order.order]
Order.MeetTheory.meetIK [prf, in mathcomp.order.order]
Order.MeetTheory.meetIKC [prf, in mathcomp.order.order]
Order.MeetTheory.meetKI [prf, in mathcomp.order.order]
Order.MeetTheory.meetKIC [prf, in mathcomp.order.order]
Order.MeetTheory.meetxx [prf, in mathcomp.order.order]
Order.mem_enum [prf, in mathcomp.order.preorder]
Order.mono_sorted_enum [prf, in mathcomp.order.preorder]
Order.mono_unique [prf, in mathcomp.order.order]
Order.NatDvd.dvdE [prf, in mathcomp.order.preorder]
Order.NatDvd.dvdn_anti [prf, in mathcomp.order.order]
Order.NatDvd.gcdE [prf, in mathcomp.order.order]
Order.NatDvd.joinKI [prf, in mathcomp.order.order]
Order.NatDvd.lcmE [prf, in mathcomp.order.order]
Order.NatDvd.lcmnn [prf, in mathcomp.order.order]
Order.NatDvd.le_def [prf, in mathcomp.order.order]
Order.NatDvd.meetKU [prf, in mathcomp.order.order]
Order.NatDvd.meetUl [prf, in mathcomp.order.order]
Order.NatDvd.nat0E [prf, in mathcomp.order.preorder]
Order.NatDvd.nat1E [prf, in mathcomp.order.preorder]
Order.NatDvd.sdvdE [prf, in mathcomp.order.order]
Order.NatMonotonyTheory.decn_inP [prf, in mathcomp.order.order]
Order.NatMonotonyTheory.decnP [prf, in mathcomp.order.order]
Order.NatMonotonyTheory.homo_ltn_lt [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.homo_ltn_lt_in [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.incn_inP [prf, in mathcomp.order.order]
Order.NatMonotonyTheory.incnP [prf, in mathcomp.order.order]
Order.NatMonotonyTheory.nhomo_ltn_lt [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.nhomo_ltn_lt_in [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.nondecn_inP [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.nondecnP [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.nonincn_inP [prf, in mathcomp.order.preorder]
Order.NatMonotonyTheory.nonincnP [prf, in mathcomp.order.preorder]
Order.NatOrder.botEnat [prf, in mathcomp.order.preorder]
Order.NatOrder.leEnat [prf, in mathcomp.order.preorder]
Order.NatOrder.ltEnat [prf, in mathcomp.order.preorder]
Order.NatOrder.ltn_def [prf, in mathcomp.order.preorder]
Order.NatOrder.maxEnat [prf, in mathcomp.order.preorder]
Order.NatOrder.minEnat [prf, in mathcomp.order.preorder]
Order.NatOrder.nat_display [prf, in mathcomp.order.preorder]
Order.nth_enum_ord [prf, in mathcomp.order.preorder]
Order.nth_ord_enum [prf, in mathcomp.order.preorder]
Order.omorph_lt [prf, in mathcomp.order.order]
Order.OrderMorphismTheory.comp_is_nondecreasing [prf, in mathcomp.order.preorder]
Order.OrderMorphismTheory.idfun_is_nondecreasing [prf, in mathcomp.order.preorder]
Order.OrderMorphismTheory.omorph_le [prf, in mathcomp.order.preorder]
Order.OrdinalOrder.botEord [prf, in mathcomp.order.preorder]
Order.OrdinalOrder.leEord [prf, in mathcomp.order.preorder]
Order.OrdinalOrder.ltEord [prf, in mathcomp.order.preorder]
Order.OrdinalOrder.ord_display [prf, in mathcomp.order.preorder]
Order.OrdinalOrder.topEord [prf, in mathcomp.order.preorder]
Order.POrderTheory.bigmax_le [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_eq_maxl [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_eq_minr [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_le_max2 [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_le_min2 [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_leP [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_lteifNE [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_ltgtP [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_ltP [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_max_idPl [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_max_minl [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxAC [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxACA [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxC [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxCA [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxEge [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_maxEgt [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_min_idPr [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_min_maxr [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minAC [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minACA [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minC [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minCA [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minEge [prf, in mathcomp.order.order]
Order.POrderTheory.comparable_minEgt [prf, in mathcomp.order.order]
Order.POrderTheory.comparableP [prf, in mathcomp.order.order]
Order.POrderTheory.contra_le_leq [prf, in mathcomp.order.order]
Order.POrderTheory.contra_le_ltn [prf, in mathcomp.order.order]
Order.POrderTheory.contra_le_not [prf, in mathcomp.order.order]
Order.POrderTheory.contra_leF [prf, in mathcomp.order.order]
Order.POrderTheory.contra_leN [prf, in mathcomp.order.order]
Order.POrderTheory.contra_leT [prf, in mathcomp.order.order]
Order.POrderTheory.contra_lt_leq [prf, in mathcomp.order.order]
Order.POrderTheory.contra_lt_ltn [prf, in mathcomp.order.order]
Order.POrderTheory.contra_lt_not [prf, in mathcomp.order.order]
Order.POrderTheory.contra_ltF [prf, in mathcomp.order.order]
Order.POrderTheory.contra_ltN [prf, in mathcomp.order.order]
Order.POrderTheory.contra_ltT [prf, in mathcomp.order.order]
Order.POrderTheory.count_lt_le_mem [prf, in mathcomp.order.order]
Order.POrderTheory.dec_inj [prf, in mathcomp.order.order]
Order.POrderTheory.dec_inj_in [prf, in mathcomp.order.order]
Order.POrderTheory.eq_geP [prf, in mathcomp.order.order]
Order.POrderTheory.eq_le [prf, in mathcomp.order.order]
Order.POrderTheory.eq_leP [prf, in mathcomp.order.order]
Order.POrderTheory.eq_maxr [prf, in mathcomp.order.order]
Order.POrderTheory.eq_minl [prf, in mathcomp.order.order]
Order.POrderTheory.ge_anti [prf, in mathcomp.order.order]
Order.POrderTheory.ge_leif [prf, in mathcomp.order.order]
Order.POrderTheory.inc_inj [prf, in mathcomp.order.order]
Order.POrderTheory.inc_inj_in [prf, in mathcomp.order.order]
Order.POrderTheory.inj_homo_lt [prf, in mathcomp.order.order]
Order.POrderTheory.inj_homo_lt_in [prf, in mathcomp.order.order]
Order.POrderTheory.inj_nhomo_lt [prf, in mathcomp.order.order]
Order.POrderTheory.inj_nhomo_lt_in [prf, in mathcomp.order.order]
Order.POrderTheory.le_anti [prf, in mathcomp.order.order]
Order.POrderTheory.le_bigmin [prf, in mathcomp.order.order]
Order.POrderTheory.le_eqVlt [prf, in mathcomp.order.order]
Order.POrderTheory.le_sorted_eq [prf, in mathcomp.order.order]
Order.POrderTheory.leif_eq [prf, in mathcomp.order.order]
Order.POrderTheory.leif_le [prf, in mathcomp.order.order]
Order.POrderTheory.leif_trans [prf, in mathcomp.order.order]
Order.POrderTheory.leifP [prf, in mathcomp.order.order]
Order.POrderTheory.lt_def [prf, in mathcomp.order.order]
Order.POrderTheory.lt_leif [prf, in mathcomp.order.order]
Order.POrderTheory.lt_neqAle [prf, in mathcomp.order.order]
Order.POrderTheory.lt_sorted_uniq_le [prf, in mathcomp.order.order]
Order.POrderTheory.lteif_anti [prf, in mathcomp.order.order]
Order.POrderTheory.lteifN [prf, in mathcomp.order.order]
Order.POrderTheory.ltNleif [prf, in mathcomp.order.order]
Order.POrderTheory.ltW_homo [prf, in mathcomp.order.order]
Order.POrderTheory.ltW_homo_in [prf, in mathcomp.order.order]
Order.POrderTheory.ltW_nhomo [prf, in mathcomp.order.order]
Order.POrderTheory.ltW_nhomo_in [prf, in mathcomp.order.order]
Order.POrderTheory.max_idPr [prf, in mathcomp.order.order]
Order.POrderTheory.max_l [prf, in mathcomp.order.order]
Order.POrderTheory.max_r [prf, in mathcomp.order.order]
Order.POrderTheory.maxEle [prf, in mathcomp.order.order]
Order.POrderTheory.min_idPl [prf, in mathcomp.order.order]
Order.POrderTheory.min_l [prf, in mathcomp.order.order]
Order.POrderTheory.min_r [prf, in mathcomp.order.order]
Order.POrderTheory.minEle [prf, in mathcomp.order.order]
Order.POrderTheory.mono_in_leif [prf, in mathcomp.order.order]
Order.POrderTheory.mono_leif [prf, in mathcomp.order.order]
Order.POrderTheory.nmono_in_leif [prf, in mathcomp.order.order]
Order.POrderTheory.nmono_leif [prf, in mathcomp.order.order]
Order.PreCancelPartial.ge_trans [prf, in mathcomp.order.preorder]
Order.PreCancelPartial.lt_le_def [prf, in mathcomp.order.preorder]
Order.PreCancelPartial.refl [prf, in mathcomp.order.preorder]
Order.PreCancelPartial.trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.bigmax_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_arg_maxP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_arg_minP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_bigl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_bigr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_le_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_leq_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_leq_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_lt_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_ltn_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_ltn_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_not_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contra_not_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraFle [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraFlt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraNle [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraNlt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraPle [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraPlt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraTle [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_contraTlt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_ge_max [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_ge_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_gt_max [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_gt_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_le_max [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_le_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_leNgt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lt_max [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lt_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lteif_maxl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lteif_maxr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lteif_minl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_lteif_minr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_ltNge [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_max_minr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_maxA [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_maxKx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_maxl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_maxr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_maxxK [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_min_maxl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_minA [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_minKx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_minl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_minr [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_minxK [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparable_sym [prf, in mathcomp.order.preorder]
Order.PreorderTheory.comparablexx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.count_le_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.count_lt_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.eq_leif [prf, in mathcomp.order.preorder]
Order.PreorderTheory.eqTleif [prf, in mathcomp.order.preorder]
Order.PreorderTheory.filter_le_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.filter_lt_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.ge_comparable [prf, in mathcomp.order.preorder]
Order.PreorderTheory.ge_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.geE [prf, in mathcomp.order.preorder]
Order.PreorderTheory.gt_comparable [prf, in mathcomp.order.preorder]
Order.PreorderTheory.gt_eqF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.gtE [prf, in mathcomp.order.preorder]
Order.PreorderTheory.incomparable_eqF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.incomparable_leF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.incomparable_ltF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_comparable [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_geP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_gtF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_le_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_leP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_lt_asym [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_lt_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_path_filter [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_path_mask [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_path_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_path_pairwise [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_path_sortedE [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_sorted_filter [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_sorted_leq_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_sorted_ltn_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_sorted_mask [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_sorted_pairwise [prf, in mathcomp.order.preorder]
Order.PreorderTheory.le_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.leif_refl [prf, in mathcomp.order.preorder]
Order.PreorderTheory.leW_mono [prf, in mathcomp.order.preorder]
Order.PreorderTheory.leW_mono_in [prf, in mathcomp.order.preorder]
Order.PreorderTheory.leW_nmono [prf, in mathcomp.order.preorder]
Order.PreorderTheory.leW_nmono_in [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lexx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_asym [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_bigmin [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_comparable [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_eqF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_geF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_gtP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_le_asym [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_le_def [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_le_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_leAnge [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_ltP [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_nsym [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_path_filter [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_path_mask [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_path_min [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_path_pairwise [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_path_sortedE [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_eq [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_filter [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_is_uniq_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_leq_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_ltn_nth [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_mask [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_pairwise [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_sorted_uniq [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lt_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteif_andb [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteif_imply [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteif_orb [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteif_trans [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifNF [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifS [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifT [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifW [prf, in mathcomp.order.preorder]
Order.PreorderTheory.lteifxx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.ltW [prf, in mathcomp.order.preorder]
Order.PreorderTheory.ltxx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.max_maxKx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.max_maxxK [prf, in mathcomp.order.preorder]
Order.PreorderTheory.maxElt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.maxxx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.min_minKx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.min_minxK [prf, in mathcomp.order.preorder]
Order.PreorderTheory.minElt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.minxx [prf, in mathcomp.order.preorder]
Order.PreorderTheory.nth_count_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.nth_count_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.sort_le_id [prf, in mathcomp.order.preorder]
Order.PreorderTheory.sort_lt_id [prf, in mathcomp.order.preorder]
Order.PreorderTheory.sorted_filter_le [prf, in mathcomp.order.preorder]
Order.PreorderTheory.sorted_filter_lt [prf, in mathcomp.order.preorder]
Order.PreorderTheory.subseq_le_path [prf, in mathcomp.order.preorder]
Order.PreorderTheory.subseq_le_sorted [prf, in mathcomp.order.preorder]
Order.PreorderTheory.subseq_lt_path [prf, in mathcomp.order.preorder]
Order.PreorderTheory.subseq_lt_sorted [prf, in mathcomp.order.preorder]
Order.prod_display_unit [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.anti [prf, in mathcomp.order.order]
Order.ProdLexiOrder.botEprodlexi [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.le0x [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.leEprodlexi [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.lexi_pair [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.lt_le_def [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.ltEprodlexi [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.ltxi_pair [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.refl [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.sub_prod_lexi [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.topEprodlexi [prf, in mathcomp.order.preorder]
Order.ProdLexiOrder.total [prf, in mathcomp.order.order]
Order.ProdLexiOrder.trans [prf, in mathcomp.order.preorder]
Order.ProdOrder.anti [prf, in mathcomp.order.order]
Order.ProdOrder.botEprod [prf, in mathcomp.order.preorder]
Order.ProdOrder.codiffEprod [prf, in mathcomp.order.order]
Order.ProdOrder.complEdiff [prf, in mathcomp.order.order]
Order.ProdOrder.complEprod [prf, in mathcomp.order.order]
Order.ProdOrder.diffEprod [prf, in mathcomp.order.order]
Order.ProdOrder.diffErcompl [prf, in mathcomp.order.order]
Order.ProdOrder.joinEprod [prf, in mathcomp.order.order]
Order.ProdOrder.le0x [prf, in mathcomp.order.preorder]
Order.ProdOrder.le_pair [prf, in mathcomp.order.preorder]
Order.ProdOrder.leEprod [prf, in mathcomp.order.preorder]
Order.ProdOrder.lexI [prf, in mathcomp.order.order]
Order.ProdOrder.lt_def [prf, in mathcomp.order.preorder]
Order.ProdOrder.lt_pair [prf, in mathcomp.order.preorder]
Order.ProdOrder.lt_pair [prf, in mathcomp.order.order]
Order.ProdOrder.ltEprod [prf, in mathcomp.order.preorder]
Order.ProdOrder.ltEprod [prf, in mathcomp.order.order]
Order.ProdOrder.meetEprod [prf, in mathcomp.order.order]
Order.ProdOrder.meetUl [prf, in mathcomp.order.order]
Order.ProdOrder.rcomplEprod [prf, in mathcomp.order.order]
Order.ProdOrder.rcomplPmeet [prf, in mathcomp.order.order]
Order.ProdOrder.refl [prf, in mathcomp.order.preorder]
Order.ProdOrder.topEprod [prf, in mathcomp.order.preorder]
Order.ProdOrder.trans [prf, in mathcomp.order.preorder]
Order.seqlexi_display [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.anti [prf, in mathcomp.order.order]
Order.SeqLexiOrder.eqhead_lexiE [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.eqhead_ltxiE [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.leEseqlexi [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.lexi0s [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.lexi_cons [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.lexi_lehead [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.lexis0 [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.lt_le_def [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.ltEseqlexi [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.ltxi0s [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.ltxi_cons [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.ltxi_lehead [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.ltxis0 [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.neqhead_lexiE [prf, in mathcomp.order.order]
Order.SeqLexiOrder.neqhead_ltxiE [prf, in mathcomp.order.order]
Order.SeqLexiOrder.refl [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.sub_seqprod_lexi [prf, in mathcomp.order.preorder]
Order.SeqLexiOrder.total [prf, in mathcomp.order.order]
Order.SeqLexiOrder.trans [prf, in mathcomp.order.preorder]
Order.seqprod_display [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.anti [prf, in mathcomp.order.order]
Order.SeqProdOrder.botEseq [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.join_cons [prf, in mathcomp.order.order]
Order.SeqProdOrder.joinEseq [prf, in mathcomp.order.order]
Order.SeqProdOrder.le0s [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.le_cons [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.leEseq [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.les0 [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.leUx [prf, in mathcomp.order.order]
Order.SeqProdOrder.lexI [prf, in mathcomp.order.order]
Order.SeqProdOrder.meet_cons [prf, in mathcomp.order.order]
Order.SeqProdOrder.meetEseq [prf, in mathcomp.order.order]
Order.SeqProdOrder.meetUl [prf, in mathcomp.order.order]
Order.SeqProdOrder.refl [prf, in mathcomp.order.preorder]
Order.SeqProdOrder.trans [prf, in mathcomp.order.preorder]
Order.set_enum [prf, in mathcomp.order.preorder]
Order.SetSubsetOrder.botEsubset [prf, in mathcomp.order.order]
Order.SetSubsetOrder.complEsubset [prf, in mathcomp.order.order]
Order.SetSubsetOrder.joinEsubset [prf, in mathcomp.order.order]
Order.SetSubsetOrder.le_anti [prf, in mathcomp.order.order]
Order.SetSubsetOrder.le_def [prf, in mathcomp.order.preorder]
Order.SetSubsetOrder.leEsubset [prf, in mathcomp.order.preorder]
Order.SetSubsetOrder.meetEsubset [prf, in mathcomp.order.order]
Order.SetSubsetOrder.setIDv [prf, in mathcomp.order.order]
Order.SetSubsetOrder.setKIC [prf, in mathcomp.order.order]
Order.SetSubsetOrder.setKUC [prf, in mathcomp.order.order]
Order.SetSubsetOrder.setTDsym [prf, in mathcomp.order.order]
Order.SetSubsetOrder.subEsubset [prf, in mathcomp.order.order]
Order.SetSubsetOrder.subset_display [prf, in mathcomp.order.preorder]
Order.SetSubsetOrder.topEsubset [prf, in mathcomp.order.order]
Order.SigmaOrder.anti [prf, in mathcomp.order.order]
Order.SigmaOrder.botEsig [prf, in mathcomp.order.order]
Order.SigmaOrder.le0x [prf, in mathcomp.order.order]
Order.SigmaOrder.le_Taggedl [prf, in mathcomp.order.order]
Order.SigmaOrder.le_Taggedr [prf, in mathcomp.order.order]
Order.SigmaOrder.leEsig [prf, in mathcomp.order.order]
Order.SigmaOrder.lex1 [prf, in mathcomp.order.order]
Order.SigmaOrder.lt_le_def [prf, in mathcomp.order.order]
Order.SigmaOrder.lt_Taggedl [prf, in mathcomp.order.order]
Order.SigmaOrder.lt_Taggedr [prf, in mathcomp.order.order]
Order.SigmaOrder.ltEsig [prf, in mathcomp.order.order]
Order.SigmaOrder.refl [prf, in mathcomp.order.order]
Order.SigmaOrder.topEsig [prf, in mathcomp.order.order]
Order.SigmaOrder.total [prf, in mathcomp.order.order]
Order.SigmaOrder.trans [prf, in mathcomp.order.order]
Order.size_enum_ord [prf, in mathcomp.order.preorder]
Order.SubPreorderTheory.le_wval [prf, in mathcomp.order.preorder]
Order.SubPreorderTheory.leEsub [prf, in mathcomp.order.preorder]
Order.SubPreorderTheory.lt_val [prf, in mathcomp.order.preorder]
Order.SubPreorderTheory.lt_wval [prf, in mathcomp.order.preorder]
Order.SubPreorderTheory.ltEsub [prf, in mathcomp.order.preorder]
Order.TDistrLatticeTheory.cover_leIxl [prf, in mathcomp.order.order]
Order.TDistrLatticeTheory.cover_leIxr [prf, in mathcomp.order.order]
Order.TDistrLatticeTheory.leI2E [prf, in mathcomp.order.order]
Order.TDistrLatticeTheory.leI2l_le [prf, in mathcomp.order.order]
Order.TDistrLatticeTheory.leI2r_le [prf, in mathcomp.order.order]
Order.TDistrLatticeTheory.meets_total [prf, in mathcomp.order.order]
Order.TJoinTheory.join1x [prf, in mathcomp.order.order]
Order.TJoinTheory.joinx1 [prf, in mathcomp.order.order]
Order.TLatticeMorphismTheory.comp_is_top_morphism [prf, in mathcomp.order.order]
Order.TLatticeMorphismTheory.idfun_is_top_morphism [prf, in mathcomp.order.order]
Order.TLatticeMorphismTheory.omorph1 [prf, in mathcomp.order.order]
Order.TMeetTheory.le_meets [prf, in mathcomp.order.order]
Order.TMeetTheory.meet1x [prf, in mathcomp.order.order]
Order.TMeetTheory.meet_eq1 [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_ge [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_inf [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_inf_seq [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_max [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_max_seq [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_seq [prf, in mathcomp.order.order]
Order.TMeetTheory.meets_setU [prf, in mathcomp.order.order]
Order.TMeetTheory.meetsP [prf, in mathcomp.order.order]
Order.TMeetTheory.meetsP_seq [prf, in mathcomp.order.order]
Order.TMeetTheory.meetx1 [prf, in mathcomp.order.order]
Order.TotalTheory.arg_maxP [prf, in mathcomp.order.order]
Order.TotalTheory.arg_minP [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_eq_arg [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_eq_id [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_ge_id [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_idl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_idr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_imset [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_leP [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_ltP [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_mkcond [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_mkcondl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_mkcondr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_set1 [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_split [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_sup [prf, in mathcomp.order.order]
Order.TotalTheory.bigmax_sup_seq [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxD [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxD1 [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxID [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxIl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxIr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxU [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxUl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmaxUr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_eq_arg [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_eq_id [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_geP [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_gtP [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_idl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_idr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_imset [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_inf [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_inf_seq [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_le [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_le_cond [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_le_id [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_mkcond [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_mkcondl [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_mkcondr [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_set1 [prf, in mathcomp.order.order]
Order.TotalTheory.bigmin_split [prf, in mathcomp.order.order]
Order.TotalTheory.bigminD [prf, in mathcomp.order.order]
Order.TotalTheory.bigminD1 [prf, in mathcomp.order.order]
Order.TotalTheory.bigminID [prf, in mathcomp.order.order]
Order.TotalTheory.bigminIl [prf, in mathcomp.order.order]
Order.TotalTheory.bigminIr [prf, in mathcomp.order.order]
Order.TotalTheory.bigminU [prf, in mathcomp.order.order]
Order.TotalTheory.bigminUl [prf, in mathcomp.order.order]
Order.TotalTheory.bigminUr [prf, in mathcomp.order.order]
Order.TotalTheory.comparableT [prf, in mathcomp.order.order]
Order.TotalTheory.contra_le [prf, in mathcomp.order.order]
Order.TotalTheory.contra_le_lt [prf, in mathcomp.order.order]
Order.TotalTheory.contra_leq_le [prf, in mathcomp.order.order]
Order.TotalTheory.contra_leq_lt [prf, in mathcomp.order.order]
Order.TotalTheory.contra_lt [prf, in mathcomp.order.order]
Order.TotalTheory.contra_lt_le [prf, in mathcomp.order.order]
Order.TotalTheory.contra_ltn_le [prf, in mathcomp.order.order]
Order.TotalTheory.contra_ltn_lt [prf, in mathcomp.order.order]
Order.TotalTheory.contra_not_le [prf, in mathcomp.order.order]
Order.TotalTheory.contra_not_lt [prf, in mathcomp.order.order]
Order.TotalTheory.contraFle [prf, in mathcomp.order.order]
Order.TotalTheory.contraFlt [prf, in mathcomp.order.order]
Order.TotalTheory.contraNle [prf, in mathcomp.order.order]
Order.TotalTheory.contraNlt [prf, in mathcomp.order.order]
Order.TotalTheory.contraPle [prf, in mathcomp.order.order]
Order.TotalTheory.contraPlt [prf, in mathcomp.order.order]
Order.TotalTheory.contraTle [prf, in mathcomp.order.order]
Order.TotalTheory.contraTlt [prf, in mathcomp.order.order]
Order.TotalTheory.count_le_gt [prf, in mathcomp.order.order]
Order.TotalTheory.count_lt_ge [prf, in mathcomp.order.order]
Order.TotalTheory.DualTotalTheory.nth_count_eq [prf, in mathcomp.order.order]
Order.TotalTheory.DualTotalTheory.nth_count_ge [prf, in mathcomp.order.order]
Order.TotalTheory.DualTotalTheory.nth_count_gt [prf, in mathcomp.order.order]
Order.TotalTheory.DualTotalTheory.sorted_filter_ge [prf, in mathcomp.order.order]
Order.TotalTheory.DualTotalTheory.sorted_filter_gt [prf, in mathcomp.order.order]
Order.TotalTheory.eq_bigmax [prf, in mathcomp.order.order]
Order.TotalTheory.eq_bigmin [prf, in mathcomp.order.order]
Order.TotalTheory.eq_gtP [prf, in mathcomp.order.order]
Order.TotalTheory.eq_leLR [prf, in mathcomp.order.order]
Order.TotalTheory.eq_leRL [prf, in mathcomp.order.order]
Order.TotalTheory.eq_ltLR [prf, in mathcomp.order.order]
Order.TotalTheory.eq_ltP [prf, in mathcomp.order.order]
Order.TotalTheory.eq_ltRL [prf, in mathcomp.order.order]
Order.TotalTheory.eq_maxl [prf, in mathcomp.order.order]
Order.TotalTheory.eq_minr [prf, in mathcomp.order.order]
Order.TotalTheory.filter_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.ge_bigmin_seq [prf, in mathcomp.order.order]
Order.TotalTheory.ge_max [prf, in mathcomp.order.order]
Order.TotalTheory.ge_min [prf, in mathcomp.order.order]
Order.TotalTheory.ge_total [prf, in mathcomp.order.order]
Order.TotalTheory.gt_max [prf, in mathcomp.order.order]
Order.TotalTheory.gt_min [prf, in mathcomp.order.order]
Order.TotalTheory.joinEtotal [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax2 [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_cond [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_nat [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_nat_cond [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_ord [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_ord_cond [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmax_seq [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmin2 [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmin_nat [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmin_nat_cond [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmin_ord [prf, in mathcomp.order.order]
Order.TotalTheory.le_bigmin_ord_cond [prf, in mathcomp.order.order]
Order.TotalTheory.le_gtP [prf, in mathcomp.order.order]
Order.TotalTheory.le_ltP [prf, in mathcomp.order.order]
Order.TotalTheory.le_max [prf, in mathcomp.order.order]
Order.TotalTheory.le_max2 [prf, in mathcomp.order.order]
Order.TotalTheory.le_min [prf, in mathcomp.order.order]
Order.TotalTheory.le_min2 [prf, in mathcomp.order.order]
Order.TotalTheory.le_mono [prf, in mathcomp.order.order]
Order.TotalTheory.le_mono_in [prf, in mathcomp.order.order]
Order.TotalTheory.le_nmono [prf, in mathcomp.order.order]
Order.TotalTheory.le_nmono_in [prf, in mathcomp.order.order]
Order.TotalTheory.leIx [prf, in mathcomp.order.order]
Order.TotalTheory.leNgt [prf, in mathcomp.order.order]
Order.TotalTheory.lexU [prf, in mathcomp.order.order]
Order.TotalTheory.lt_max [prf, in mathcomp.order.order]
Order.TotalTheory.lt_min [prf, in mathcomp.order.order]
Order.TotalTheory.lt_total [prf, in mathcomp.order.order]
Order.TotalTheory.lteif_maxl [prf, in mathcomp.order.order]
Order.TotalTheory.lteif_maxr [prf, in mathcomp.order.order]
Order.TotalTheory.lteif_minl [prf, in mathcomp.order.order]
Order.TotalTheory.lteif_minr [prf, in mathcomp.order.order]
Order.TotalTheory.lteifNE [prf, in mathcomp.order.order]
Order.TotalTheory.ltIx [prf, in mathcomp.order.order]
Order.TotalTheory.ltNge [prf, in mathcomp.order.order]
Order.TotalTheory.ltUx [prf, in mathcomp.order.order]
Order.TotalTheory.ltxI [prf, in mathcomp.order.order]
Order.TotalTheory.ltxU [prf, in mathcomp.order.order]
Order.TotalTheory.mask_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.max_idPl [prf, in mathcomp.order.order]
Order.TotalTheory.max_minl [prf, in mathcomp.order.order]
Order.TotalTheory.max_minr [prf, in mathcomp.order.order]
Order.TotalTheory.maxA [prf, in mathcomp.order.order]
Order.TotalTheory.maxAC [prf, in mathcomp.order.order]
Order.TotalTheory.maxACA [prf, in mathcomp.order.order]
Order.TotalTheory.maxC [prf, in mathcomp.order.order]
Order.TotalTheory.maxCA [prf, in mathcomp.order.order]
Order.TotalTheory.maxEge [prf, in mathcomp.order.order]
Order.TotalTheory.maxEgt [prf, in mathcomp.order.order]
Order.TotalTheory.maxKx [prf, in mathcomp.order.order]
Order.TotalTheory.maxxK [prf, in mathcomp.order.order]
Order.TotalTheory.meetEtotal [prf, in mathcomp.order.order]
Order.TotalTheory.mem2_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.min_idPr [prf, in mathcomp.order.order]
Order.TotalTheory.min_maxl [prf, in mathcomp.order.order]
Order.TotalTheory.min_maxr [prf, in mathcomp.order.order]
Order.TotalTheory.minA [prf, in mathcomp.order.order]
Order.TotalTheory.minAC [prf, in mathcomp.order.order]
Order.TotalTheory.minACA [prf, in mathcomp.order.order]
Order.TotalTheory.minC [prf, in mathcomp.order.order]
Order.TotalTheory.minCA [prf, in mathcomp.order.order]
Order.TotalTheory.minEge [prf, in mathcomp.order.order]
Order.TotalTheory.minEgt [prf, in mathcomp.order.order]
Order.TotalTheory.minKx [prf, in mathcomp.order.order]
Order.TotalTheory.minxK [prf, in mathcomp.order.order]
Order.TotalTheory.neq_lt [prf, in mathcomp.order.order]
Order.TotalTheory.perm_sort_leP [prf, in mathcomp.order.order]
Order.TotalTheory.sort_le_sorted [prf, in mathcomp.order.order]
Order.TotalTheory.sort_lt_sorted [prf, in mathcomp.order.order]
Order.TotalTheory.sorted_mask_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.sorted_subseq_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmax [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmax_cond [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmax_seq [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmin [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmin_cond [prf, in mathcomp.order.order]
Order.TotalTheory.sub_bigmin_seq [prf, in mathcomp.order.order]
Order.TotalTheory.sub_in_bigmax [prf, in mathcomp.order.order]
Order.TotalTheory.sub_in_bigmin [prf, in mathcomp.order.order]
Order.TotalTheory.subseq_sort_le [prf, in mathcomp.order.order]
Order.TotalTheory.subset_bigmax [prf, in mathcomp.order.order]
Order.TotalTheory.subset_bigmax_cond [prf, in mathcomp.order.order]
Order.TotalTheory.subset_bigmin [prf, in mathcomp.order.order]
Order.TotalTheory.subset_bigmin_cond [prf, in mathcomp.order.order]
Order.TotalTheory.wlog_le [prf, in mathcomp.order.order]
Order.TotalTheory.wlog_lt [prf, in mathcomp.order.order]
Order.TPOrderTheory.le1x [prf, in mathcomp.order.order]
Order.TPOrderTheory.ltx1 [prf, in mathcomp.order.order]
Order.TPreorderTheory.lex1 [prf, in mathcomp.order.preorder]
Order.TPreorderTheory.lt1x [prf, in mathcomp.order.preorder]
Order.TupleLexiOrder.botEtlexi [prf, in mathcomp.order.preorder]
Order.TupleLexiOrder.le0x [prf, in mathcomp.order.preorder]
Order.TupleLexiOrder.lex1 [prf, in mathcomp.order.preorder]
Order.TupleLexiOrder.lexi_tupleP [prf, in mathcomp.order.order]
Order.TupleLexiOrder.ltxi_tupleP [prf, in mathcomp.order.order]
Order.TupleLexiOrder.ltxi_tuplePlt [prf, in mathcomp.order.order]
Order.TupleLexiOrder.sub_tprod_lexi [prf, in mathcomp.order.preorder]
Order.TupleLexiOrder.topEtlexi [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.botEtprod [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.codiffErcompl [prf, in mathcomp.order.order]
Order.TupleProdOrder.codiffEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.complEcodiff [prf, in mathcomp.order.order]
Order.TupleProdOrder.complEdiff [prf, in mathcomp.order.order]
Order.TupleProdOrder.complEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.diffErcompl [prf, in mathcomp.order.order]
Order.TupleProdOrder.diffEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.joinEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.le0x [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.leEtprod [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.leUx [prf, in mathcomp.order.order]
Order.TupleProdOrder.lex1 [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.lexI [prf, in mathcomp.order.order]
Order.TupleProdOrder.ltEtprod [prf, in mathcomp.order.preorder]
Order.TupleProdOrder.meetEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.meetUl [prf, in mathcomp.order.order]
Order.TupleProdOrder.rcomplEtprod [prf, in mathcomp.order.order]
Order.TupleProdOrder.rcomplPjoin [prf, in mathcomp.order.order]
Order.TupleProdOrder.rcomplPmeet [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_codiff [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_compl [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_diff [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_join [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_meet [prf, in mathcomp.order.order]
Order.TupleProdOrder.tnth_rcompl [prf, in mathcomp.order.order]
Order.TupleProdOrder.topEtprod [prf, in mathcomp.order.preorder]
Order.val_enum_ord [prf, in mathcomp.order.preorder]
order1 [prf, in mathcomp.finite_group.fingroup]
order_constt [prf, in mathcomp.solvable.pgroup]
order_cycle [prf, in mathcomp.boot.fingraph]
order_dvdG [prf, in mathcomp.solvable.cyclic]
order_dvdn [prf, in mathcomp.solvable.cyclic]
order_eq1 [prf, in mathcomp.finite_group.fingroup]
order_finv [prf, in mathcomp.boot.fingraph]
order_gt0 [prf, in mathcomp.finite_group.fingroup]
order_gt0 [prf, in mathcomp.boot.fingraph]
order_gt1 [prf, in mathcomp.finite_group.fingroup]
order_id [prf, in mathcomp.boot.fingraph]
order_id_cycle [prf, in mathcomp.boot.fingraph]
order_inf [prf, in mathcomp.solvable.cyclic]
order_inj_cyclic [prf, in mathcomp.solvable.cyclic]
order_injm [prf, in mathcomp.finite_group.morphism]
order_le_cycle [prf, in mathcomp.boot.fingraph]
order_path_min [prf, in mathcomp.boot.path]
order_path_min_in [prf, in mathcomp.boot.path]
order_pprimeChar [prf, in mathcomp.field.finfield]
order_set_finv [prf, in mathcomp.boot.fingraph]
order_Zp1 [prf, in mathcomp.algebra.zmodp]
orderE [prf, in mathcomp.finite_group.fingroup]
orderJ [prf, in mathcomp.finite_group.fingroup]
orderM [prf, in mathcomp.solvable.cyclic]
orderPcycle [prf, in mathcomp.boot.fingraph]
orderSpred [prf, in mathcomp.boot.fingraph]
orderV [prf, in mathcomp.finite_group.fingroup]
orderXdiv [prf, in mathcomp.solvable.cyclic]
orderXdvd [prf, in mathcomp.solvable.cyclic]
orderXexp [prf, in mathcomp.solvable.cyclic]
orderXgcd [prf, in mathcomp.solvable.cyclic]
orderXpfactor [prf, in mathcomp.solvable.cyclic]
orderXpnat [prf, in mathcomp.solvable.cyclic]
orderXprime [prf, in mathcomp.solvable.cyclic]
ordS_bij [prf, in mathcomp.boot.fintype]
ordS_inj [prf, in mathcomp.boot.fintype]
ordSK [prf, in mathcomp.boot.fintype]
ortho_id [prf, in mathcomp.algebra.spectral]
ortho_mx_ortho [prf, in mathcomp.algebra.sesquilinear]
ortho_ortho_mx [prf, in mathcomp.algebra.sesquilinear]
orthoDmx [prf, in mathcomp.algebra.sesquilinear]
orthoDv [prf, in mathcomp.algebra.sesquilinear]
orthogonal1P [prf, in mathcomp.algebra.sesquilinear]
orthogonal_catl [prf, in mathcomp.group_representation.classfun]
orthogonal_catl [prf, in mathcomp.algebra.sesquilinear]
orthogonal_catr [prf, in mathcomp.group_representation.classfun]
orthogonal_catr [prf, in mathcomp.algebra.sesquilinear]
orthogonal_cons [prf, in mathcomp.group_representation.classfun]
orthogonal_cons [prf, in mathcomp.algebra.sesquilinear]
orthogonal_free [prf, in mathcomp.group_representation.classfun]
orthogonal_free [prf, in mathcomp.algebra.sesquilinear]
orthogonal_oppl [prf, in mathcomp.group_representation.classfun]
orthogonal_oppl [prf, in mathcomp.algebra.sesquilinear]
orthogonal_oppr [prf, in mathcomp.group_representation.classfun]
orthogonal_oppr [prf, in mathcomp.algebra.sesquilinear]
orthogonal_span [prf, in mathcomp.group_representation.vcharacter]
orthogonal_split [prf, in mathcomp.group_representation.classfun]
orthogonal_split [prf, in mathcomp.algebra.sesquilinear]
orthogonal_sym [prf, in mathcomp.group_representation.classfun]
orthogonal_sym [prf, in mathcomp.algebra.sesquilinear]
orthogonalE [prf, in mathcomp.algebra.sesquilinear]
orthogonalP [prf, in mathcomp.group_representation.classfun]
orthogonalP [prf, in mathcomp.algebra.sesquilinear]
orthomx1E [prf, in mathcomp.algebra.spectral]
orthomx1P [prf, in mathcomp.algebra.spectral]
orthomx_disj [prf, in mathcomp.algebra.spectral]
orthomx_ortho_disj [prf, in mathcomp.algebra.spectral]
orthomx_proj_mx_ortho [prf, in mathcomp.algebra.spectral]
orthomx_spectralP [prf, in mathcomp.algebra.spectral]
orthomx_sym [prf, in mathcomp.algebra.sesquilinear]
orthomxD [prf, in mathcomp.algebra.sesquilinear]
orthomxE [prf, in mathcomp.algebra.sesquilinear]
orthomxN [prf, in mathcomp.algebra.sesquilinear]
orthomxP [prf, in mathcomp.algebra.sesquilinear]
orthomxZ [prf, in mathcomp.algebra.sesquilinear]
orthoNmx [prf, in mathcomp.algebra.sesquilinear]
orthonormal2P [prf, in mathcomp.group_representation.classfun]
orthonormal2P [prf, in mathcomp.algebra.sesquilinear]
orthonormal_cat [prf, in mathcomp.group_representation.classfun]
orthonormal_cat [prf, in mathcomp.algebra.sesquilinear]
orthonormal_free [prf, in mathcomp.group_representation.classfun]
orthonormal_free [prf, in mathcomp.algebra.sesquilinear]
orthonormal_not0 [prf, in mathcomp.group_representation.classfun]
orthonormal_not0 [prf, in mathcomp.algebra.sesquilinear]
orthonormal_orthogonal [prf, in mathcomp.group_representation.classfun]
orthonormal_orthogonal [prf, in mathcomp.algebra.sesquilinear]
orthonormal_span [prf, in mathcomp.group_representation.vcharacter]
orthonormalE [prf, in mathcomp.group_representation.classfun]
orthonormalE [prf, in mathcomp.algebra.sesquilinear]
orthonormalP [prf, in mathcomp.group_representation.classfun]
orthonormalP [prf, in mathcomp.algebra.sesquilinear]
orthoP [prf, in mathcomp.group_representation.classfun]
orthoP [prf, in mathcomp.algebra.sesquilinear]
orthoPl [prf, in mathcomp.group_representation.classfun]
orthoPl [prf, in mathcomp.algebra.sesquilinear]
orthoPr [prf, in mathcomp.group_representation.classfun]
orthoPr [prf, in mathcomp.algebra.sesquilinear]
orthov0 [prf, in mathcomp.algebra.sesquilinear]
orthov11 [prf, in mathcomp.algebra.sesquilinear]
orthov1E [prf, in mathcomp.algebra.sesquilinear]
orthov_sym [prf, in mathcomp.algebra.sesquilinear]
orthovD [prf, in mathcomp.algebra.sesquilinear]
orthovE [prf, in mathcomp.algebra.sesquilinear]
orthovP [prf, in mathcomp.algebra.sesquilinear]
orthoZmx [prf, in mathcomp.algebra.sesquilinear]
ostack_eqE [prf, in mathcomp.algebra.tensor]
ostack_tupleE [prf, in mathcomp.algebra.tensor]
ostackE [prf, in mathcomp.algebra.tensor]
otensor_eqP [prf, in mathcomp.algebra.tensor]
otensor_of_tupleE [prf, in mathcomp.algebra.tensor]
otensor_of_tupleK [prf, in mathcomp.algebra.tensor]
otensorP [prf, in mathcomp.algebra.tensor]
out_Aut [prf, in mathcomp.finite_group.automorphism]
out_perm [prf, in mathcomp.finite_group.perm]