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

Notation 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 | _ | other | (999 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 | _ | other | (811 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 | _ | other | (1769 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 | _ | other | (588 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 | _ | other | (11879 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 | _ | other | (960 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 | _ | other | (508 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 | _ | other | (307 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 | _ | other | (479 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 | _ | other | (495 entries) |

Instance 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 | _ | other | (905 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 | _ | other | (1199 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 | _ | other | (4894 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 | _ | other | (166 entries) |

## B (lemma)

Backport_OT.lt_trans [in Coq.Structures.OrdersAlt]Backport_OT.lt_not_eq [in Coq.Structures.OrdersAlt]

Backport_Sets.lt_not_eq [in Coq.FSets.FSetCompat]

BalanceProps.append_arb_rb [in Coq.MSets.MSetRBT]

BalanceProps.arb_nr_rb [in Coq.MSets.MSetRBT]

BalanceProps.arb_nrr_rb [in Coq.MSets.MSetRBT]

BalanceProps.del_rb [in Coq.MSets.MSetRBT]

BalanceProps.del_arb [in Coq.MSets.MSetRBT]

BalanceProps.diff_rb [in Coq.MSets.MSetRBT]

BalanceProps.ifred_or [in Coq.MSets.MSetRBT]

BalanceProps.ifred_notred [in Coq.MSets.MSetRBT]

BalanceProps.ins_arb [in Coq.MSets.MSetRBT]

BalanceProps.ins_rr_rb [in Coq.MSets.MSetRBT]

BalanceProps.inter_rb [in Coq.MSets.MSetRBT]

BalanceProps.lbalS_arb [in Coq.MSets.MSetRBT]

BalanceProps.lbalS_rb [in Coq.MSets.MSetRBT]

BalanceProps.lbal_rb [in Coq.MSets.MSetRBT]

BalanceProps.makeBlack_rb [in Coq.MSets.MSetRBT]

BalanceProps.makeRed_rr [in Coq.MSets.MSetRBT]

BalanceProps.maxdepth_lowerbound [in Coq.MSets.MSetRBT]

BalanceProps.maxdepth_upperbound [in Coq.MSets.MSetRBT]

BalanceProps.rbalS_arb [in Coq.MSets.MSetRBT]

BalanceProps.rbalS_rb [in Coq.MSets.MSetRBT]

BalanceProps.rbal_rb [in Coq.MSets.MSetRBT]

BalanceProps.rbal'_rb [in Coq.MSets.MSetRBT]

BalanceProps.rb_mindepth [in Coq.MSets.MSetRBT]

BalanceProps.rb_maxdepth [in Coq.MSets.MSetRBT]

BalanceProps.rr_nrr_rb [in Coq.MSets.MSetRBT]

BalanceProps.singleton_rb [in Coq.MSets.MSetRBT]

BalanceProps.treeify_aux_rb [in Coq.MSets.MSetRBT]

BalanceProps.treeify_cont_rb [in Coq.MSets.MSetRBT]

BalanceProps.treeify_one_rb [in Coq.MSets.MSetRBT]

BalanceProps.treeify_zero_rb [in Coq.MSets.MSetRBT]

BalanceProps.union_rb [in Coq.MSets.MSetRBT]

Ball_in_inter [in Coq.Reals.PSeries_reg]

base_Int_part [in Coq.Reals.R_Ifp]

base_fp [in Coq.Reals.R_Ifp]

between_not_exists [in Coq.Arith.Between]

between_or_exists [in Coq.Arith.Between]

between_in_int [in Coq.Arith.Between]

between_restr [in Coq.Arith.Between]

between_Sk_l [in Coq.Arith.Between]

between_le [in Coq.Arith.Between]

bet_eq [in Coq.Arith.Between]

bezout_rel_prime [in Coq.ZArith.Znumtheory]

BijComp_FunctExt [in Coq.Logic.ExtensionalityFacts]

bij_can_bij [in Coq.ssr.ssrfun]

bij_comp [in Coq.ssr.ssrfun]

bij_can_eq [in Coq.ssr.ssrfun]

bij_can_sym [in Coq.ssr.ssrfun]

bij_inj [in Coq.ssr.ssrfun]

bind_unless [in Coq.ssr.ssrbool]

bInjective_bSurjective [in Coq.Logic.FinFun]

binomial [in Coq.Reals.Binomial]

bitE [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_add_or [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_0 [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_lsl [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_ext [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_half [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_M [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_1 [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_b2i [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_lsr [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_split [in Coq.Numbers.Cyclic.Int63.Uint63]

bit_0_spec [in Coq.Numbers.Cyclic.Int63.Uint63]

Bolzano_Weierstrass [in Coq.Reals.Rtopology]

boolean_witness_nonzero [in Coq.btauto.Reflect]

BoolEqualityFacts.eqb_sym [in Coq.Structures.Equalities]

BoolEqualityFacts.eqb_refl [in Coq.Structures.Equalities]

BoolEqualityFacts.eqb_neq [in Coq.Structures.Equalities]

BoolEqualityFacts.eqb_spec [in Coq.Structures.Equalities]

BoolOrderFacts.eqb_compare [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_compare [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_antisym [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_refl [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_gt [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_nle [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_spec [in Coq.Structures.OrdersFacts]

BoolOrderFacts.leb_spec0 [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_compare [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_antisym [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_irrefl [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_ge [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_nlt [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_spec [in Coq.Structures.OrdersFacts]

BoolOrderFacts.ltb_spec0 [in Coq.Structures.OrdersFacts]

boolP [in Coq.ssr.ssrbool]

BoolTheory [in Coq.setoid_ring.Ring]

bool_eq_ok [in Coq.setoid_ring.Ring]

bool_choice [in Coq.Init.Specif]

bool_dec [in Coq.Bool.Bool]

Boule_center [in Coq.Reals.PSeries_reg]

Boule_convex [in Coq.Reals.PSeries_reg]

Boule_lt [in Coq.Reals.Ratan]

Boule_half_to_interval [in Coq.Reals.Ratan]

bSurjective_bBijective [in Coq.Logic.FinFun]

byte_of_ascii_via_nat [in Coq.Strings.Ascii]

byte_of_ascii_via_N [in Coq.Strings.Ascii]

byte_of_ascii_of_byte [in Coq.Strings.Ascii]

byte_dec_bl [in Coq.Strings.Byte]

byte_dec_lb [in Coq.Strings.Byte]

B1_cvg [in Coq.Reals.Cos_rel]

b2n_b2z [in Coq.micromega.ZifyBool]

b2z_spec [in Coq.micromega.ZifyBool]

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

Notation 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 | _ | other | (999 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 | _ | other | (811 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 | _ | other | (1769 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 | _ | other | (588 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 | _ | other | (11879 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 | _ | other | (960 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 | _ | other | (508 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 | _ | other | (307 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 | _ | other | (479 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 | _ | other | (495 entries) |

Instance 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 | _ | other | (905 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 | _ | other | (1199 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 | _ | other | (4894 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 | _ | other | (166 entries) |