| 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 | (18818 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 | (548 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 | (206 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 | (68 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 | (8939 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 | (338 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 | (422 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 | (644 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 | (1243 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 | (209 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 | (2935 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 | (703 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 | (699 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 | (1456 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 | (408 entries) |
Q
Q [record, in Coq.QArith.QArith_base]Q [module, in Coq.QArith.Qminmax]
Qabs [definition, in Coq.QArith.Qabs]
Qabs [library]
Qabs_diff_Qle_condition [lemma, in Coq.QArith.Qabs]
Qabs_Qle_condition [lemma, in Coq.QArith.Qabs]
Qabs_triangle_reverse [lemma, in Coq.QArith.Qabs]
Qabs_Qminus [lemma, in Coq.QArith.Qabs]
Qabs_Qmult [lemma, in Coq.QArith.Qabs]
Qabs_triangle [lemma, in Coq.QArith.Qabs]
Qabs_opp [lemma, in Coq.QArith.Qabs]
Qabs_nonneg [lemma, in Coq.QArith.Qabs]
Qabs_neg [lemma, in Coq.QArith.Qabs]
Qabs_pos [lemma, in Coq.QArith.Qabs]
Qabs_case [lemma, in Coq.QArith.Qabs]
QArith [library]
QArith_base [library]
Qc [record, in Coq.QArith.Qcanon]
Qcanon [library]
Qccompare [definition, in Coq.QArith.Qcanon]
Qcdiv [definition, in Coq.QArith.Qcanon]
Qcdiv_mult_l [lemma, in Coq.QArith.Qcanon]
Qceiling [definition, in Coq.QArith.Qround]
Qceiling_resp_le [lemma, in Coq.QArith.Qround]
Qceiling_lt [lemma, in Coq.QArith.Qround]
Qceiling_Z [lemma, in Coq.QArith.Qround]
Qceq_alt [lemma, in Coq.QArith.Qcanon]
Qcft [definition, in Coq.QArith.Qcanon]
Qcge [abbreviation, in Coq.QArith.Qcanon]
Qcgt [abbreviation, in Coq.QArith.Qcanon]
Qcgt_alt [lemma, in Coq.QArith.Qcanon]
Qcinv [definition, in Coq.QArith.Qcanon]
Qcinv_mult_distr [lemma, in Coq.QArith.Qcanon]
Qcle [definition, in Coq.QArith.Qcanon]
Qcle_minus_iff [lemma, in Coq.QArith.Qcanon]
Qcle_lt_or_eq [lemma, in Coq.QArith.Qcanon]
Qcle_not_lt [lemma, in Coq.QArith.Qcanon]
Qcle_lt_trans [lemma, in Coq.QArith.Qcanon]
Qcle_trans [lemma, in Coq.QArith.Qcanon]
Qcle_antisym [lemma, in Coq.QArith.Qcanon]
Qcle_refl [lemma, in Coq.QArith.Qcanon]
Qclt [definition, in Coq.QArith.Qcanon]
Qclt_minus_iff [lemma, in Coq.QArith.Qcanon]
Qclt_le_dec [lemma, in Coq.QArith.Qcanon]
Qclt_not_le [lemma, in Coq.QArith.Qcanon]
Qclt_trans [lemma, in Coq.QArith.Qcanon]
Qclt_le_trans [lemma, in Coq.QArith.Qcanon]
Qclt_le_weak [lemma, in Coq.QArith.Qcanon]
Qclt_not_eq [lemma, in Coq.QArith.Qcanon]
Qclt_alt [lemma, in Coq.QArith.Qcanon]
Qcmake [constructor, in Coq.QArith.Qcanon]
Qcminus [definition, in Coq.QArith.Qcanon]
Qcmult [definition, in Coq.QArith.Qcanon]
Qcmult_lt_compat_r [lemma, in Coq.QArith.Qcanon]
Qcmult_lt_0_le_reg_r [lemma, in Coq.QArith.Qcanon]
Qcmult_le_compat_r [lemma, in Coq.QArith.Qcanon]
Qcmult_div_r [lemma, in Coq.QArith.Qcanon]
Qcmult_inv_l [lemma, in Coq.QArith.Qcanon]
Qcmult_inv_r [lemma, in Coq.QArith.Qcanon]
Qcmult_integral_l [lemma, in Coq.QArith.Qcanon]
Qcmult_integral [lemma, in Coq.QArith.Qcanon]
Qcmult_plus_distr_l [lemma, in Coq.QArith.Qcanon]
Qcmult_plus_distr_r [lemma, in Coq.QArith.Qcanon]
Qcmult_comm [lemma, in Coq.QArith.Qcanon]
Qcmult_1_r [lemma, in Coq.QArith.Qcanon]
Qcmult_1_l [lemma, in Coq.QArith.Qcanon]
Qcmult_assoc [lemma, in Coq.QArith.Qcanon]
Qcnot_le_lt [lemma, in Coq.QArith.Qcanon]
Qcnot_lt_le [lemma, in Coq.QArith.Qcanon]
Qcompare [definition, in Coq.QArith.QArith_base]
Qcompare_comp [instance, in Coq.QArith.QArith_base]
Qcompare_spec [lemma, in Coq.QArith.QArith_base]
Qcompare_antisym [lemma, in Coq.QArith.QArith_base]
Qcopp [definition, in Coq.QArith.Qcanon]
Qcopp_le_compat [lemma, in Coq.QArith.Qcanon]
Qcopp_involutive [lemma, in Coq.QArith.Qcanon]
Qcplus [definition, in Coq.QArith.Qcanon]
Qcplus_le_compat [lemma, in Coq.QArith.Qcanon]
Qcplus_opp_r [lemma, in Coq.QArith.Qcanon]
Qcplus_comm [lemma, in Coq.QArith.Qcanon]
Qcplus_0_r [lemma, in Coq.QArith.Qcanon]
Qcplus_0_l [lemma, in Coq.QArith.Qcanon]
Qcplus_assoc [lemma, in Coq.QArith.Qcanon]
Qcpower [definition, in Coq.QArith.Qcanon]
Qcpower_pos [lemma, in Coq.QArith.Qcanon]
Qcpower_0 [lemma, in Coq.QArith.Qcanon]
Qcpower_1 [lemma, in Coq.QArith.Qcanon]
Qcrt [definition, in Coq.QArith.Qcanon]
Qc_decomp [lemma, in Coq.QArith.Qcanon]
Qc_eq_bool_correct [lemma, in Coq.QArith.Qcanon]
Qc_eq_bool [definition, in Coq.QArith.Qcanon]
Qc_dec [lemma, in Coq.QArith.Qcanon]
Qc_eq_dec [lemma, in Coq.QArith.Qcanon]
Qc_is_canon [lemma, in Coq.QArith.Qcanon]
QDen [abbreviation, in Coq.QArith.QArith_base]
Qden [projection, in Coq.QArith.QArith_base]
Qdiv [definition, in Coq.QArith.QArith_base]
Qdiv_mult_l [lemma, in Coq.QArith.QArith_base]
Qdiv_comp [instance, in Coq.QArith.QArith_base]
Qdiv_power [lemma, in Coq.QArith.Qpower]
Qeq [definition, in Coq.QArith.QArith_base]
Qeqb_comp [instance, in Coq.QArith.QArith_base]
Qeq_bool_neq [lemma, in Coq.QArith.QArith_base]
Qeq_eq_bool [lemma, in Coq.QArith.QArith_base]
Qeq_bool_eq [lemma, in Coq.QArith.QArith_base]
Qeq_bool_iff [lemma, in Coq.QArith.QArith_base]
Qeq_bool [definition, in Coq.QArith.QArith_base]
Qeq_dec [lemma, in Coq.QArith.QArith_base]
Qeq_trans [lemma, in Coq.QArith.QArith_base]
Qeq_sym [lemma, in Coq.QArith.QArith_base]
Qeq_refl [lemma, in Coq.QArith.QArith_base]
Qeq_alt [lemma, in Coq.QArith.QArith_base]
Qeq_eqR [lemma, in Coq.QArith.Qreals]
Qfield [library]
Qfloor [definition, in Coq.QArith.Qround]
Qfloor_resp_le [lemma, in Coq.QArith.Qround]
Qfloor_le [lemma, in Coq.QArith.Qround]
Qfloor_Z [lemma, in Coq.QArith.Qround]
Qge [abbreviation, in Coq.QArith.QArith_base]
Qge_alt [lemma, in Coq.QArith.QArith_base]
Qge_alt [lemma, in Coq.QArith.Qcanon]
Qgt [abbreviation, in Coq.QArith.QArith_base]
Qgt_alt [lemma, in Coq.QArith.QArith_base]
QHasMinMax [module, in Coq.QArith.Qminmax]
QHasMinMax.max [definition, in Coq.QArith.Qminmax]
QHasMinMax.max_r [definition, in Coq.QArith.Qminmax]
QHasMinMax.max_l [definition, in Coq.QArith.Qminmax]
QHasMinMax.min [definition, in Coq.QArith.Qminmax]
QHasMinMax.min_r [definition, in Coq.QArith.Qminmax]
QHasMinMax.min_l [definition, in Coq.QArith.Qminmax]
QHasMinMax.QMM [module, in Coq.QArith.Qminmax]
Qinv [definition, in Coq.QArith.QArith_base]
Qinv_lt_0_compat [lemma, in Coq.QArith.QArith_base]
Qinv_le_0_compat [lemma, in Coq.QArith.QArith_base]
Qinv_mult_distr [lemma, in Coq.QArith.QArith_base]
Qinv_involutive [lemma, in Coq.QArith.QArith_base]
Qinv_comp [instance, in Coq.QArith.QArith_base]
Qinv_power_n [lemma, in Coq.QArith.Qpower]
Qinv_power [lemma, in Coq.QArith.Qpower]
Qinv_power_positive [lemma, in Coq.QArith.Qpower]
Qle [definition, in Coq.QArith.QArith_base]
Qleb_comp [instance, in Coq.QArith.QArith_base]
Qle_shift_inv_r [lemma, in Coq.QArith.QArith_base]
Qle_shift_div_r [lemma, in Coq.QArith.QArith_base]
Qle_shift_inv_l [lemma, in Coq.QArith.QArith_base]
Qle_shift_div_l [lemma, in Coq.QArith.QArith_base]
Qle_minus_iff [lemma, in Coq.QArith.QArith_base]
Qle_lt_or_eq [lemma, in Coq.QArith.QArith_base]
Qle_not_lt [lemma, in Coq.QArith.QArith_base]
Qle_lt_trans [lemma, in Coq.QArith.QArith_base]
Qle_lteq [lemma, in Coq.QArith.QArith_base]
Qle_trans [lemma, in Coq.QArith.QArith_base]
Qle_antisym [lemma, in Coq.QArith.QArith_base]
Qle_refl [lemma, in Coq.QArith.QArith_base]
Qle_comp [instance, in Coq.QArith.QArith_base]
Qle_bool_imp_le [lemma, in Coq.QArith.QArith_base]
Qle_bool_iff [lemma, in Coq.QArith.QArith_base]
Qle_bool [definition, in Coq.QArith.QArith_base]
Qle_alt [lemma, in Coq.QArith.QArith_base]
Qle_Rle [lemma, in Coq.QArith.Qreals]
Qle_floor_ceiling [lemma, in Coq.QArith.Qround]
Qle_ceiling [lemma, in Coq.QArith.Qround]
Qle_alt [lemma, in Coq.QArith.Qcanon]
Qle_Qabs [lemma, in Coq.QArith.Qabs]
Qlt [definition, in Coq.QArith.QArith_base]
Qlt_shift_inv_r [lemma, in Coq.QArith.QArith_base]
Qlt_shift_div_r [lemma, in Coq.QArith.QArith_base]
Qlt_shift_inv_l [lemma, in Coq.QArith.QArith_base]
Qlt_shift_div_l [lemma, in Coq.QArith.QArith_base]
Qlt_minus_iff [lemma, in Coq.QArith.QArith_base]
Qlt_le_dec [lemma, in Coq.QArith.QArith_base]
Qlt_not_le [lemma, in Coq.QArith.QArith_base]
Qlt_trans [lemma, in Coq.QArith.QArith_base]
Qlt_le_trans [lemma, in Coq.QArith.QArith_base]
Qlt_le_weak [lemma, in Coq.QArith.QArith_base]
Qlt_not_eq [lemma, in Coq.QArith.QArith_base]
Qlt_irrefl [lemma, in Coq.QArith.QArith_base]
Qlt_compat [instance, in Coq.QArith.QArith_base]
Qlt_alt [lemma, in Coq.QArith.QArith_base]
Qlt_Rlt [lemma, in Coq.QArith.Qreals]
Qlt_floor [lemma, in Coq.QArith.Qround]
Qmake [constructor, in Coq.QArith.QArith_base]
QMake [library]
Qmake_Qdiv [lemma, in Coq.QArith.QArith_base]
Qmax [definition, in Coq.QArith.Qminmax]
Qmin [definition, in Coq.QArith.Qminmax]
Qminmax [library]
Qminus [definition, in Coq.QArith.QArith_base]
Qminus_comp [instance, in Coq.QArith.QArith_base]
Qminus' [definition, in Coq.QArith.Qreduction]
Qminus'_correct [lemma, in Coq.QArith.Qreduction]
Qmult [definition, in Coq.QArith.QArith_base]
Qmult_le_0_compat [lemma, in Coq.QArith.QArith_base]
Qmult_lt_l [lemma, in Coq.QArith.QArith_base]
Qmult_lt_r [lemma, in Coq.QArith.QArith_base]
Qmult_lt_compat_r [lemma, in Coq.QArith.QArith_base]
Qmult_le_l [lemma, in Coq.QArith.QArith_base]
Qmult_le_r [lemma, in Coq.QArith.QArith_base]
Qmult_lt_0_le_reg_r [lemma, in Coq.QArith.QArith_base]
Qmult_le_compat_r [lemma, in Coq.QArith.QArith_base]
Qmult_inj_l [lemma, in Coq.QArith.QArith_base]
Qmult_inj_r [lemma, in Coq.QArith.QArith_base]
Qmult_div_r [lemma, in Coq.QArith.QArith_base]
Qmult_inv_r [lemma, in Coq.QArith.QArith_base]
Qmult_integral_l [lemma, in Coq.QArith.QArith_base]
Qmult_integral [lemma, in Coq.QArith.QArith_base]
Qmult_plus_distr_l [lemma, in Coq.QArith.QArith_base]
Qmult_plus_distr_r [lemma, in Coq.QArith.QArith_base]
Qmult_comm [lemma, in Coq.QArith.QArith_base]
Qmult_1_r [lemma, in Coq.QArith.QArith_base]
Qmult_1_l [lemma, in Coq.QArith.QArith_base]
Qmult_0_r [lemma, in Coq.QArith.QArith_base]
Qmult_0_l [lemma, in Coq.QArith.QArith_base]
Qmult_assoc [lemma, in Coq.QArith.QArith_base]
Qmult_comp [instance, in Coq.QArith.QArith_base]
Qmult_power [lemma, in Coq.QArith.Qpower]
Qmult_power_positive [lemma, in Coq.QArith.Qpower]
Qmult' [definition, in Coq.QArith.Qreduction]
Qmult'_correct [lemma, in Coq.QArith.Qreduction]
Qnot_le_lt [lemma, in Coq.QArith.QArith_base]
Qnot_lt_le [lemma, in Coq.QArith.QArith_base]
Qnot_eq_sym [lemma, in Coq.QArith.QArith_base]
Qnum [projection, in Coq.QArith.QArith_base]
Qopp [definition, in Coq.QArith.QArith_base]
Qopp_opp [lemma, in Coq.QArith.Qfield]
Qopp_plus [lemma, in Coq.QArith.Qfield]
Qopp_le_compat [lemma, in Coq.QArith.QArith_base]
Qopp_involutive [lemma, in Coq.QArith.QArith_base]
Qopp_comp [instance, in Coq.QArith.QArith_base]
Qopp_lt_compat [lemma, in Coq.QArith.Qround]
QOrder [module, in Coq.QArith.QOrderedType]
QOrderedType [library]
Qplus [definition, in Coq.QArith.QArith_base]
Qplus_lt_r [lemma, in Coq.QArith.QArith_base]
Qplus_lt_l [lemma, in Coq.QArith.QArith_base]
Qplus_le_r [lemma, in Coq.QArith.QArith_base]
Qplus_le_l [lemma, in Coq.QArith.QArith_base]
Qplus_lt_le_compat [lemma, in Coq.QArith.QArith_base]
Qplus_le_compat [lemma, in Coq.QArith.QArith_base]
Qplus_inj_l [lemma, in Coq.QArith.QArith_base]
Qplus_inj_r [lemma, in Coq.QArith.QArith_base]
Qplus_opp_r [lemma, in Coq.QArith.QArith_base]
Qplus_comm [lemma, in Coq.QArith.QArith_base]
Qplus_0_r [lemma, in Coq.QArith.QArith_base]
Qplus_0_l [lemma, in Coq.QArith.QArith_base]
Qplus_assoc [lemma, in Coq.QArith.QArith_base]
Qplus_comp [instance, in Coq.QArith.QArith_base]
Qplus' [definition, in Coq.QArith.Qreduction]
Qplus'_correct [lemma, in Coq.QArith.Qreduction]
Qpower [definition, in Coq.QArith.QArith_base]
Qpower [library]
Qpower_theory [lemma, in Coq.QArith.Qfield]
Qpower_comp [instance, in Coq.QArith.QArith_base]
Qpower_positive_comp [instance, in Coq.QArith.QArith_base]
Qpower_positive [definition, in Coq.QArith.QArith_base]
Qpower_decomp [lemma, in Coq.QArith.Qpower]
Qpower_mult [lemma, in Coq.QArith.Qpower]
Qpower_mult_positive [lemma, in Coq.QArith.Qpower]
Qpower_plus' [lemma, in Coq.QArith.Qpower]
Qpower_plus [lemma, in Coq.QArith.Qpower]
Qpower_minus_positive [lemma, in Coq.QArith.Qpower]
Qpower_opp [lemma, in Coq.QArith.Qpower]
Qpower_plus_positive [lemma, in Coq.QArith.Qpower]
Qpower_pos [lemma, in Coq.QArith.Qpower]
Qpower_pos_positive [lemma, in Coq.QArith.Qpower]
Qpower_not_0_positive [lemma, in Coq.QArith.Qpower]
Qpower_0 [lemma, in Coq.QArith.Qpower]
Qpower_positive_0 [lemma, in Coq.QArith.Qpower]
Qpower_1 [lemma, in Coq.QArith.Qpower]
Qpower_positive_1 [lemma, in Coq.QArith.Qpower]
QProperties [module, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.add_opp_diag_r [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.add_assoc [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.add_comm [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.add_0_l [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.add_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.compare_spec [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.compare_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.div_mul_inv [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.div_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eqb [definition, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eqb_complete [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eqb_correct [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eqb_eq [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eq_bool_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.eq_equiv [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.inv_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.le_lteq [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.le_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.lt_total [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.lt_strorder [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.lt_compat [definition, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.lt_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.max_r [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.max_l [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.max_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.min_r [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.min_l [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.min_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_inv_diag_l [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_add_distr_r [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_assoc [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_comm [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_1_l [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.mul_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.neq_1_0 [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.opp_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.power_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.red_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.square_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.sub_add_opp [lemma, in Coq.Numbers.Rational.SpecViaQ.QSig]
QProperties.sub_wd [instance, in Coq.Numbers.Rational.SpecViaQ.QSig]
Qreals [library]
Qred [definition, in Coq.QArith.Qreduction]
Qreduction [library]
Qred_compare [lemma, in Coq.QArith.Qreduction]
Qred_opp [lemma, in Coq.QArith.Qreduction]
Qred_complete [lemma, in Coq.QArith.Qreduction]
Qred_correct [lemma, in Coq.QArith.Qreduction]
Qred_involutive [lemma, in Coq.QArith.Qcanon]
Qred_iff [lemma, in Coq.QArith.Qcanon]
Qred_identity2 [lemma, in Coq.QArith.Qcanon]
Qred_identity [lemma, in Coq.QArith.Qcanon]
Qring [library]
Qround [library]
Qsft [definition, in Coq.QArith.Qfield]
QSig [library]
Qsqr_nonneg [lemma, in Coq.QArith.Qpower]
Qsrt [definition, in Coq.QArith.Qfield]
QType [module, in Coq.Numbers.Rational.SpecViaQ.QSig]
QTypeExt [module, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ ^ _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
/ _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ / _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
- _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ * _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ - _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ + _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
1 [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
0 [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ < _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ <= _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ != _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
_ == _ [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
[ _ ] [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType_Notation [module, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType' [module, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.add [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.compare [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.div [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.eq [definition, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.eq_bool [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.inv [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.le [definition, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.lt [definition, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.max [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.min [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.minus_one [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.mul [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.of_Q [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.one [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.opp [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.power [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.red [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_power [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_div [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_inv [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_square [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_mul [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_opp [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_sub [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_add [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_m1 [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_1 [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_0 [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_min [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_max [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_eq_bool [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_compare [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_red [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.spec_of_Q [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.square [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.strong_spec_red [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.sub [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.t [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.to_Q [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
QType.zero [axiom, in Coq.Numbers.Rational.SpecViaQ.QSig]
[ _ ] [notation, in Coq.Numbers.Rational.SpecViaQ.QSig]
quadruple [lemma, in Coq.Reals.Ranalysis2]
quadruple_var [lemma, in Coq.Reals.Ranalysis2]
quotient [lemma, in Coq.Arith.Euclid]
quotient_by_2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
QuotRem [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
_ rem _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
_ รท _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.quot_rem [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.quot_wd [instance, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_opp_r [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_opp_l [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_bound_pos [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_wd [instance, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem.quot [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem.rem [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
Q_dec [lemma, in Coq.QArith.QArith_base]
Q_apart_0_1 [lemma, in Coq.QArith.QArith_base]
Q_Setoid [instance, in Coq.QArith.QArith_base]
Q_as_OT.compare_spec [definition, in Coq.QArith.QOrderedType]
Q_as_OT.le_lteq [definition, in Coq.QArith.QOrderedType]
Q_as_OT.lt_compat [instance, in Coq.QArith.QOrderedType]
Q_as_OT.lt_strorder [instance, in Coq.QArith.QOrderedType]
Q_as_OT.compare [definition, in Coq.QArith.QOrderedType]
Q_as_OT.le [definition, in Coq.QArith.QOrderedType]
Q_as_OT.lt [definition, in Coq.QArith.QOrderedType]
Q_as_OT [module, in Coq.QArith.QOrderedType]
Q_as_DT.eqb_eq [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eqb [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eq_equiv [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eq [definition, in Coq.QArith.QOrderedType]
Q_as_DT.t [definition, in Coq.QArith.QOrderedType]
Q_as_DT [module, in Coq.QArith.QOrderedType]
Q_apart_0_1 [lemma, in Coq.QArith.Qcanon]
Q.plus_min_distr_r [lemma, in Coq.QArith.Qminmax]
Q.plus_min_distr_l [lemma, in Coq.QArith.Qminmax]
Q.plus_max_distr_r [lemma, in Coq.QArith.Qminmax]
Q.plus_max_distr_l [lemma, in Coq.QArith.Qminmax]
Q2Qc [definition, in Coq.QArith.Qcanon]
Q2R [definition, in Coq.QArith.Qreals]
Q2R_div [lemma, in Coq.QArith.Qreals]
Q2R_inv [lemma, in Coq.QArith.Qreals]
Q2R_minus [lemma, in Coq.QArith.Qreals]
Q2R_opp [lemma, in Coq.QArith.Qreals]
Q2R_mult [lemma, in Coq.QArith.Qreals]
Q2R_plus [lemma, in Coq.QArith.Qreals]
| 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 | (18818 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 | (548 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 | (206 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 | (68 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 | (8939 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 | (338 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 | (422 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 | (644 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 | (1243 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 | (209 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 | (2935 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 | (703 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 | (699 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 | (1456 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 | (408 entries) |