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 | (21799 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 | (910 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 | (727 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |

## T (lemma)

tail031_equiv [in Coq.Numbers.Cyclic.Int31.Cyclic31]take_prf_irr [in Coq.Vectors.VectorSpec]

take_app [in Coq.Vectors.VectorSpec]

take_idem [in Coq.Vectors.VectorSpec]

take_O [in Coq.Vectors.VectorSpec]

tan_2PI3 [in Coq.Reals.Rtrigo_calc]

tan_PI3 [in Coq.Reals.Rtrigo_calc]

tan_PI6 [in Coq.Reals.Rtrigo_calc]

tan_PI4 [in Coq.Reals.Rtrigo_calc]

tan_2PI [in Coq.Reals.Rtrigo_calc]

tan_PI [in Coq.Reals.Rtrigo_calc]

tan_incr_1 [in Coq.Reals.Rtrigo1]

tan_incr_0 [in Coq.Reals.Rtrigo1]

tan_increasing_1 [in Coq.Reals.Rtrigo1]

tan_increasing_0 [in Coq.Reals.Rtrigo1]

tan_diff [in Coq.Reals.Rtrigo1]

tan_lt_0 [in Coq.Reals.Rtrigo1]

tan_gt_0 [in Coq.Reals.Rtrigo1]

tan_minus [in Coq.Reals.Rtrigo1]

tan_neg [in Coq.Reals.Rtrigo1]

tan_0 [in Coq.Reals.Rtrigo1]

tan_2a [in Coq.Reals.Rtrigo1]

tan_plus [in Coq.Reals.Rtrigo1]

tan_1_gt_1 [in Coq.Reals.Ratan]

tan_is_inj [in Coq.Reals.Ratan]

tan_increasing [in Coq.Reals.Ratan]

tauto_checker_sound [in Coq.micromega.Tauto]

tech [in Coq.Reals.Machin]

tech_single_z_r_R1 [in Coq.Reals.RIneq]

tech_Rgt_minus [in Coq.Reals.RIneq]

tech_Rplus [in Coq.Reals.RIneq]

tech_up [in Coq.Reals.R_Ifp]

tech_limit_contr [in Coq.Reals.Rlimit]

tech_limit [in Coq.Reals.Rlimit]

tech_pow_Rplus [in Coq.Reals.Rfunctions]

tech_pow_Rmult [in Coq.Reals.Rfunctions]

tech_opp_tan [in Coq.Reals.Ratan]

tech1 [in Coq.Reals.PartSum]

tech11 [in Coq.Reals.PartSum]

tech12 [in Coq.Reals.PartSum]

tech13 [in Coq.Reals.SeqProp]

tech2 [in Coq.Reals.PartSum]

tech3 [in Coq.Reals.PartSum]

tech4 [in Coq.Reals.PartSum]

tech5 [in Coq.Reals.PartSum]

tech6 [in Coq.Reals.PartSum]

tech7 [in Coq.Reals.PartSum]

tech8 [in Coq.Reals.ArithProp]

tech9 [in Coq.Reals.SeqProp]

Tget_Tmap [in Coq.rtauto.Bintree]

Tget_Tadd [in Coq.rtauto.Bintree]

Tget_Tempty [in Coq.rtauto.Bintree]

tl_nth_tl [in Coq.Lists.Streams]

Tmap_Tadd [in Coq.rtauto.Bintree]

TOMaxEqDec_to_Compare.compare_spec [in Coq.Structures.GenericMinMax]

topredE [in Coq.ssr.ssrbool]

toRad_inj [in Coq.Reals.Rtrigo_calc]

to_list_of_list_opp [in Coq.Vectors.VectorSpec]

to_pos_of_pos [in Coq.Strings.BinaryString]

to_nat_of_nat [in Coq.Strings.BinaryString]

to_N_of_N [in Coq.Strings.BinaryString]

to_nat_inj [in Coq.Vectors.Fin]

to_nat_of_nat [in Coq.Vectors.Fin]

to_pos_of_pos [in Coq.Strings.OctalString]

to_nat_of_nat [in Coq.Strings.OctalString]

to_Z_of_Z [in Coq.Strings.OctalString]

to_N_of_N [in Coq.Strings.OctalString]

to_pos_of_pos [in Coq.Strings.HexString]

to_nat_of_nat [in Coq.Strings.HexString]

to_Z_of_Z [in Coq.Strings.HexString]

to_N_of_N [in Coq.Strings.HexString]

to_int_surj [in Coq.Numbers.DecimalZ]

to_int_inj [in Coq.Numbers.DecimalZ]

to_of [in Coq.Numbers.DecimalZ]

translation_0 [in Coq.Reals.Rgeom]

trans_EqSt [in Coq.Lists.Streams]

trans_sym_eq [in Coq.Logic.Eqdep_dec]

trans_eq_bool [in Coq.Bool.Bool]

treesort [in Coq.Sorting.Heap]

treesort_twist2 [in Coq.Sets.Multiset]

treesort_twist1 [in Coq.Sets.Multiset]

treesort_twist2 [in Coq.Sets.Uniset]

treesort_twist1 [in Coq.Sets.Uniset]

triangle [in Coq.Reals.Rgeom]

triangle_rectangle_le [in Coq.Reals.R_sqr]

triangle_rectangle_lt [in Coq.Reals.R_sqr]

triangle_rectangle [in Coq.Reals.R_sqr]

Triple_as_Couple_Singleton [in Coq.Sets.Powerset_facts]

Triple_as_Couple [in Coq.Sets.Powerset_facts]

Triple_as_union [in Coq.Sets.Powerset_facts]

triv_nat [in Coq.Sets.Integers]

triv_div_th [in Coq.setoid_ring.InitialRing]

trunc [in Coq.Vectors.VectorDef]

TTLB_to_OTF.eqb_eq [in Coq.Structures.Orders]

TTLB_to_OTF.compare_spec [in Coq.Structures.Orders]

twice_or_twice_plus_one [in Coq.Numbers.Cyclic.Int31.Cyclic31]

twice_zero [in Coq.Numbers.Cyclic.Int31.Cyclic31]

twist [in Coq.Sets.Permut]

two_p_pred [in Coq.ZArith.Zpower]

two_p_S [in Coq.ZArith.Zpower]

two_p_gt_ZERO [in Coq.ZArith.Zpower]

two_p_is_exp [in Coq.ZArith.Zpower]

two_p_correct [in Coq.ZArith.Zpower]

two_power_pos_is_exp [in Coq.ZArith.Zpower]

two_power_pos_correct [in Coq.ZArith.Zpower]

two_power_pos_nat [in Coq.ZArith.Zpower]

two_power_nat_correct [in Coq.ZArith.Zpower]

two_power_nat_S [in Coq.ZArith.Zpower]

two_p_equiv [in Coq.ZArith.Zpower]

two_power_pos_equiv [in Coq.ZArith.Zpower]

two_power_nat_equiv [in Coq.ZArith.Zpower]

two_p_power2 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]

two_compl_to_Z_to_two_compl [in Coq.ZArith.Zdigits]

two_compl_value_Sn [in Coq.ZArith.Zdigits]

two_compl_value [in Coq.ZArith.Zdigits]

TypeNeqSmallType.paradox [in Coq.Logic.Hurkens]

TypeNeqSmallType.up_down [in Coq.Logic.Hurkens]

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 | (21799 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 | (910 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 | (727 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |