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 | _ | (6599 entries) |

Projection 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 | _ | (86 entries) |

Record 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 | _ | (57 entries) |

Lemma 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 | _ | (3455 entries) |

Section 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 | _ | (290 entries) |

Constructor 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 | _ | (147 entries) |

Abbreviation 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 | _ | (148 entries) |

Inductive 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 | _ | (53 entries) |

Definition 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 | _ | (1466 entries) |

Axiom 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 | _ | (28 entries) |

Module 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 | _ | (53 entries) |

Variable 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 | _ | (788 entries) |

Library 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 | _ | (28 entries) |

## O (lemma)

oddb [in ssrnat]odd_add [in ssrnat]

odd_double [in ssrnat]

odd_double_half [in ssrnat]

odd_exp [in ssrnat]

odd_lift_perm [in matrix]

odd_mod [in div]

odd_mul [in ssrnat]

odd_mul_tperm [in perm]

odd_opp [in ssrnat]

odd_permJ [in perm]

odd_permM [in perm]

odd_permV [in perm]

odd_perm1 [in perm]

odd_perm_prod [in perm]

odd_sub [in ssrnat]

odd_tperm [in perm]

odd_2'nat [in prime]

onA_bij [in ssrbool]

onW_bij [in ssrbool]

on1A [in ssrbool]

on1lA [in ssrbool]

on1lW [in ssrbool]

on1W [in ssrbool]

on2A [in ssrbool]

on2W [in ssrbool]

on_can_inj [in ssrbool]

on_card_preimset [in finset]

option_enumP [in fintype]

opt_eqP [in eqtype]

orbA [in ssrbool]

orbAC [in ssrbool]

orbb [in ssrbool]

orbC [in ssrbool]

orbCA [in ssrbool]

orbF [in ssrbool]

orbit_rot_cycle [in connect]

orbit_uniq [in connect]

orbK [in ssrbool]

orbN [in ssrbool]

orbT [in ssrbool]

orb_andl [in ssrbool]

orb_andr [in ssrbool]

orderJ [in groups]

orderM [in cyclic]

orderSpred [in connect]

orderV [in groups]

orderXdiv [in cyclic]

orderXdvd [in cyclic]

orderXgcd [in cyclic]

order1 [in groups]

order_cycle [in connect]

order_div_card [in connect]

order_dvdG [in cyclic]

order_dvdn [in cyclic]

order_eq1 [in cyclic]

order_finv [in connect]

order_gt0 [in groups]

order_inf [in cyclic]

order_inj_cyclic [in cyclic]

order_path_min [in paths]

order_set_finv [in connect]

ord1 [in zmodp]

ord_enum_uniq [in fintype]

ord_inj [in fintype]

ord_maxP [in fintype]

ord_oppK [in fintype]

ord_subP [in fintype]

orFb [in ssrbool]

orKb [in ssrbool]

orNb [in ssrbool]

orP [in ssrbool]

orTb [in ssrbool]

or3P [in ssrbool]

or4P [in ssrbool]

out_Aut [in automorphism]

out_perm [in perm]

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 | _ | (6599 entries) |

Projection 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 | _ | (86 entries) |

Record 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 | _ | (57 entries) |

Lemma 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 | _ | (3455 entries) |

Section 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 | _ | (290 entries) |

Constructor 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 | _ | (147 entries) |

Abbreviation 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 | _ | (148 entries) |

Inductive 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 | _ | (53 entries) |

Definition 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 | _ | (1466 entries) |

Axiom 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 | _ | (28 entries) |

Module 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 | _ | (53 entries) |

Variable 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 | _ | (788 entries) |

Library 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 | _ | (28 entries) |