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 (26071 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 (1003 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 (815 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 (1771 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 (589 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 (961 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 (12021 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 (308 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 (496 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 (906 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 (1204 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 (4844 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)

Q (lemma)

Qabs_Qgt_condition [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qabs_Rabs [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qabs_gt [in Stdlib.QArith.Qabs]
Qabs_ge [in Stdlib.QArith.Qabs]
Qabs_diff_Qlt_condition [in Stdlib.QArith.Qabs]
Qabs_diff_Qle_condition [in Stdlib.QArith.Qabs]
Qabs_Qlt_condition [in Stdlib.QArith.Qabs]
Qabs_Qle_condition [in Stdlib.QArith.Qabs]
Qabs_triangle_reverse [in Stdlib.QArith.Qabs]
Qabs_Qminus [in Stdlib.QArith.Qabs]
Qabs_Qinv [in Stdlib.QArith.Qabs]
Qabs_Qmult [in Stdlib.QArith.Qabs]
Qabs_triangle [in Stdlib.QArith.Qabs]
Qabs_opp [in Stdlib.QArith.Qabs]
Qabs_nonneg [in Stdlib.QArith.Qabs]
Qabs_neg [in Stdlib.QArith.Qabs]
Qabs_pos [in Stdlib.QArith.Qabs]
Qabs_case [in Stdlib.QArith.Qabs]
Qabs_involutive [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
Qarchimedean [in Stdlib.QArith.QArith_base]
Qarchimedean_power2_pos [in Stdlib.QArith.Qpower]
Qbound_ltabs_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_4 [in Stdlib.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_3 [in Stdlib.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_2 [in Stdlib.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_1 [in Stdlib.Reals.Cauchy.QExtra]
Qbound_leabs_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qbound_le_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qcabs_null [in Stdlib.QArith.Qcabs]
Qcabs_diff_Qcle_condition [in Stdlib.QArith.Qcabs]
Qcabs_Qcle_condition [in Stdlib.QArith.Qcabs]
Qcabs_triangle_reverse [in Stdlib.QArith.Qcabs]
Qcabs_Qcminus [in Stdlib.QArith.Qcabs]
Qcabs_Qcmult [in Stdlib.QArith.Qcabs]
Qcabs_triangle [in Stdlib.QArith.Qcabs]
Qcabs_opp [in Stdlib.QArith.Qcabs]
Qcabs_nonneg [in Stdlib.QArith.Qcabs]
Qcabs_neg [in Stdlib.QArith.Qcabs]
Qcabs_pos [in Stdlib.QArith.Qcabs]
Qcabs_case [in Stdlib.QArith.Qcabs]
Qcabs_canon [in Stdlib.QArith.Qcabs]
Qcdiv_mult_l [in Stdlib.QArith.Qcanon]
Qceiling_resp_le [in Stdlib.QArith.Qround]
Qceiling_lt [in Stdlib.QArith.Qround]
Qceiling_Z [in Stdlib.QArith.Qround]
Qceq_alt [in Stdlib.QArith.Qcanon]
Qcge_alt [in Stdlib.QArith.Qcanon]
Qcgt_alt [in Stdlib.QArith.Qcanon]
Qcinv_mult_distr [in Stdlib.QArith.Qcanon]
Qcle_minus_iff [in Stdlib.QArith.Qcanon]
Qcle_lt_or_eq [in Stdlib.QArith.Qcanon]
Qcle_not_lt [in Stdlib.QArith.Qcanon]
Qcle_lt_trans [in Stdlib.QArith.Qcanon]
Qcle_trans [in Stdlib.QArith.Qcanon]
Qcle_antisym [in Stdlib.QArith.Qcanon]
Qcle_refl [in Stdlib.QArith.Qcanon]
Qcle_alt [in Stdlib.QArith.Qcanon]
Qcle_Qcabs [in Stdlib.QArith.Qcabs]
Qclt_minus_iff [in Stdlib.QArith.Qcanon]
Qclt_le_dec [in Stdlib.QArith.Qcanon]
Qclt_not_le [in Stdlib.QArith.Qcanon]
Qclt_trans [in Stdlib.QArith.Qcanon]
Qclt_le_trans [in Stdlib.QArith.Qcanon]
Qclt_le_weak [in Stdlib.QArith.Qcanon]
Qclt_not_eq [in Stdlib.QArith.Qcanon]
Qclt_alt [in Stdlib.QArith.Qcanon]
Qcmult_lt_compat_r [in Stdlib.QArith.Qcanon]
Qcmult_lt_0_le_reg_r [in Stdlib.QArith.Qcanon]
Qcmult_le_compat_r [in Stdlib.QArith.Qcanon]
Qcmult_div_r [in Stdlib.QArith.Qcanon]
Qcmult_inv_l [in Stdlib.QArith.Qcanon]
Qcmult_inv_r [in Stdlib.QArith.Qcanon]
Qcmult_integral_l [in Stdlib.QArith.Qcanon]
Qcmult_integral [in Stdlib.QArith.Qcanon]
Qcmult_plus_distr_l [in Stdlib.QArith.Qcanon]
Qcmult_plus_distr_r [in Stdlib.QArith.Qcanon]
Qcmult_comm [in Stdlib.QArith.Qcanon]
Qcmult_1_r [in Stdlib.QArith.Qcanon]
Qcmult_1_l [in Stdlib.QArith.Qcanon]
Qcmult_0_r [in Stdlib.QArith.Qcanon]
Qcmult_0_l [in Stdlib.QArith.Qcanon]
Qcmult_assoc [in Stdlib.QArith.Qcanon]
Qcnot_le_lt [in Stdlib.QArith.Qcanon]
Qcnot_lt_le [in Stdlib.QArith.Qcanon]
Qcompare_spec [in Stdlib.QArith.QArith_base]
Qcompare_antisym [in Stdlib.QArith.QArith_base]
Qcopp_le_compat [in Stdlib.QArith.Qcanon]
Qcopp_involutive [in Stdlib.QArith.Qcanon]
Qcplus_le_compat [in Stdlib.QArith.Qcanon]
Qcplus_opp_r [in Stdlib.QArith.Qcanon]
Qcplus_comm [in Stdlib.QArith.Qcanon]
Qcplus_0_r [in Stdlib.QArith.Qcanon]
Qcplus_0_l [in Stdlib.QArith.Qcanon]
Qcplus_assoc [in Stdlib.QArith.Qcanon]
Qcpower_pos [in Stdlib.QArith.Qcanon]
Qcpower_0 [in Stdlib.QArith.Qcanon]
Qcpower_1 [in Stdlib.QArith.Qcanon]
Qc_eq_bool_correct [in Stdlib.QArith.Qcanon]
Qc_dec [in Stdlib.QArith.Qcanon]
Qc_eq_dec [in Stdlib.QArith.Qcanon]
Qc_decomp [in Stdlib.QArith.Qcanon]
Qc_is_canon [in Stdlib.QArith.Qcanon]
Qden_cancel [in Stdlib.QArith.QArith_base]
Qdiv_mult_l [in Stdlib.QArith.QArith_base]
Qdiv_power [in Stdlib.QArith.Qpower]
Qeq_bool_trans [in Stdlib.QArith.QArith_base]
Qeq_bool_sym [in Stdlib.QArith.QArith_base]
Qeq_bool_refl [in Stdlib.QArith.QArith_base]
Qeq_bool_comm [in Stdlib.QArith.QArith_base]
Qeq_bool_neq [in Stdlib.QArith.QArith_base]
Qeq_eq_bool [in Stdlib.QArith.QArith_base]
Qeq_bool_eq [in Stdlib.QArith.QArith_base]
Qeq_bool_iff [in Stdlib.QArith.QArith_base]
Qeq_dec [in Stdlib.QArith.QArith_base]
Qeq_trans [in Stdlib.QArith.QArith_base]
Qeq_sym [in Stdlib.QArith.QArith_base]
Qeq_refl [in Stdlib.QArith.QArith_base]
Qeq_alt [in Stdlib.QArith.QArith_base]
Qeq_false [in Stdlib.micromega.RMicromega]
Qeq_true [in Stdlib.micromega.RMicromega]
Qeq_eqR [in Stdlib.QArith.Qreals]
Qeval_nformula_dec [in Stdlib.micromega.QMicromega]
Qeval_formula_compat [in Stdlib.micromega.QMicromega]
Qeval_op2_hold [in Stdlib.micromega.QMicromega]
Qeval_expr_compat [in Stdlib.micromega.QMicromega]
Qeval_expr_simpl [in Stdlib.micromega.QMicromega]
Qfloor_resp_le [in Stdlib.QArith.Qround]
Qfloor_le [in Stdlib.QArith.Qround]
Qfloor_Z [in Stdlib.QArith.Qround]
Qge_le [in Stdlib.QArith.QArith_base]
Qge_alt [in Stdlib.QArith.QArith_base]
Qgt_lt [in Stdlib.QArith.QArith_base]
Qgt_alt [in Stdlib.QArith.QArith_base]
Qinv_lt_contravar [in Stdlib.QArith.QArith_base]
Qinv_lt_0_compat [in Stdlib.QArith.QArith_base]
Qinv_le_0_compat [in Stdlib.QArith.QArith_base]
Qinv_minus_distr [in Stdlib.QArith.QArith_base]
Qinv_plus_distr [in Stdlib.QArith.QArith_base]
Qinv_neg [in Stdlib.QArith.QArith_base]
Qinv_pos [in Stdlib.QArith.QArith_base]
Qinv_mult_distr [in Stdlib.QArith.QArith_base]
Qinv_involutive [in Stdlib.QArith.QArith_base]
Qinv_power_n [in Stdlib.QArith.Qpower]
Qinv_power [in Stdlib.QArith.Qpower]
Qinv_power_positive [in Stdlib.QArith.Qpower]
Qle_shift_inv_r [in Stdlib.QArith.QArith_base]
Qle_shift_div_r [in Stdlib.QArith.QArith_base]
Qle_shift_inv_l [in Stdlib.QArith.QArith_base]
Qle_shift_div_l [in Stdlib.QArith.QArith_base]
Qle_minus_iff [in Stdlib.QArith.QArith_base]
Qle_lt_or_eq [in Stdlib.QArith.QArith_base]
Qle_not_lt [in Stdlib.QArith.QArith_base]
Qle_lt_trans [in Stdlib.QArith.QArith_base]
Qle_ge [in Stdlib.QArith.QArith_base]
Qle_lteq [in Stdlib.QArith.QArith_base]
Qle_trans [in Stdlib.QArith.QArith_base]
Qle_antisym [in Stdlib.QArith.QArith_base]
Qle_refl [in Stdlib.QArith.QArith_base]
Qle_bool_imp_le [in Stdlib.QArith.QArith_base]
Qle_bool_iff [in Stdlib.QArith.QArith_base]
Qle_alt [in Stdlib.QArith.QArith_base]
Qle_true [in Stdlib.micromega.RMicromega]
Qle_trans_swap_hyp [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qle_Qabs [in Stdlib.QArith.Qabs]
Qle_floor_ceiling [in Stdlib.QArith.Qround]
Qle_ceiling [in Stdlib.QArith.Qround]
Qle_Rle [in Stdlib.QArith.Qreals]
Qlowbound_ltabs_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qlowbound_lt_ZExp2_spec [in Stdlib.Reals.Cauchy.QExtra]
Qlowbound_ltabs_ZExp2_opp [in Stdlib.Reals.Cauchy.QExtra]
Qlowbound_ltabs_ZExp2_inv [in Stdlib.Reals.Cauchy.QExtra]
Qlt_shift_inv_r [in Stdlib.QArith.QArith_base]
Qlt_shift_div_r [in Stdlib.QArith.QArith_base]
Qlt_shift_inv_l [in Stdlib.QArith.QArith_base]
Qlt_shift_div_l [in Stdlib.QArith.QArith_base]
Qlt_minus_iff [in Stdlib.QArith.QArith_base]
Qlt_le_dec [in Stdlib.QArith.QArith_base]
Qlt_not_le [in Stdlib.QArith.QArith_base]
Qlt_trans [in Stdlib.QArith.QArith_base]
Qlt_le_trans [in Stdlib.QArith.QArith_base]
Qlt_gt [in Stdlib.QArith.QArith_base]
Qlt_le_weak [in Stdlib.QArith.QArith_base]
Qlt_leneq [in Stdlib.QArith.QArith_base]
Qlt_not_eq [in Stdlib.QArith.QArith_base]
Qlt_irrefl [in Stdlib.QArith.QArith_base]
Qlt_alt [in Stdlib.QArith.QArith_base]
Qlt_bool_iff [in Stdlib.micromega.QMicromega]
Qlt_trans_swap_hyp [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qlt_floor [in Stdlib.QArith.Qround]
Qlt_Rlt [in Stdlib.QArith.Qreals]
Qmake_Qdiv [in Stdlib.QArith.QArith_base]
Qminus'_correct [in Stdlib.QArith.Qreduction]
Qmult_le_compat_nonneg [in Stdlib.QArith.QArith_base]
Qmult_le_lt_compat_pos [in Stdlib.QArith.QArith_base]
Qmult_lt_compat_nonneg [in Stdlib.QArith.QArith_base]
Qmult_lt_1_compat [in Stdlib.QArith.QArith_base]
Qmult_le_1_compat [in Stdlib.QArith.QArith_base]
Qmult_lt_0_compat [in Stdlib.QArith.QArith_base]
Qmult_le_0_compat [in Stdlib.QArith.QArith_base]
Qmult_lt_l [in Stdlib.QArith.QArith_base]
Qmult_lt_r [in Stdlib.QArith.QArith_base]
Qmult_lt_compat_r [in Stdlib.QArith.QArith_base]
Qmult_le_l [in Stdlib.QArith.QArith_base]
Qmult_le_r [in Stdlib.QArith.QArith_base]
Qmult_lt_0_le_reg_r [in Stdlib.QArith.QArith_base]
Qmult_le_compat_r [in Stdlib.QArith.QArith_base]
Qmult_frac_r [in Stdlib.QArith.QArith_base]
Qmult_frac_l [in Stdlib.QArith.QArith_base]
Qmult_inject_Z_r [in Stdlib.QArith.QArith_base]
Qmult_inject_Z_l [in Stdlib.QArith.QArith_base]
Qmult_inj_l [in Stdlib.QArith.QArith_base]
Qmult_inj_r [in Stdlib.QArith.QArith_base]
Qmult_div_r [in Stdlib.QArith.QArith_base]
Qmult_inv_r [in Stdlib.QArith.QArith_base]
Qmult_integral_l [in Stdlib.QArith.QArith_base]
Qmult_integral [in Stdlib.QArith.QArith_base]
Qmult_plus_distr_l [in Stdlib.QArith.QArith_base]
Qmult_plus_distr_r [in Stdlib.QArith.QArith_base]
Qmult_comm [in Stdlib.QArith.QArith_base]
Qmult_1_r [in Stdlib.QArith.QArith_base]
Qmult_1_l [in Stdlib.QArith.QArith_base]
Qmult_0_r [in Stdlib.QArith.QArith_base]
Qmult_0_l [in Stdlib.QArith.QArith_base]
Qmult_assoc [in Stdlib.QArith.QArith_base]
Qmult_integral [in Stdlib.micromega.RMicromega]
Qmult_power [in Stdlib.QArith.Qpower]
Qmult_power_positive [in Stdlib.QArith.Qpower]
Qmult'_correct [in Stdlib.QArith.Qreduction]
Qnot_le_lt [in Stdlib.QArith.QArith_base]
Qnot_lt_le [in Stdlib.QArith.QArith_base]
Qnot_eq_sym [in Stdlib.QArith.QArith_base]
Qnot_lt_iff_le [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qnot_le_iff_lt [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
QNpower [in Stdlib.micromega.QMicromega]
Qnum_cancel [in Stdlib.QArith.QArith_base]
Qopp_lt_compat [in Stdlib.QArith.QArith_base]
Qopp_le_compat [in Stdlib.QArith.QArith_base]
Qopp_involutive [in Stdlib.QArith.QArith_base]
Qopp_mult_mone [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
Qopp_opp [in Stdlib.QArith.Qfield]
Qopp_plus [in Stdlib.QArith.Qfield]
Qplus_lt_compat [in Stdlib.QArith.QArith_base]
Qplus_lt_r [in Stdlib.QArith.QArith_base]
Qplus_lt_l [in Stdlib.QArith.QArith_base]
Qplus_le_r [in Stdlib.QArith.QArith_base]
Qplus_le_l [in Stdlib.QArith.QArith_base]
Qplus_lt_le_compat [in Stdlib.QArith.QArith_base]
Qplus_le_compat [in Stdlib.QArith.QArith_base]
Qplus_inj_l [in Stdlib.QArith.QArith_base]
Qplus_inj_r [in Stdlib.QArith.QArith_base]
Qplus_opp_r [in Stdlib.QArith.QArith_base]
Qplus_comm [in Stdlib.QArith.QArith_base]
Qplus_0_r [in Stdlib.QArith.QArith_base]
Qplus_0_l [in Stdlib.QArith.QArith_base]
Qplus_assoc [in Stdlib.QArith.QArith_base]
Qplus'_correct [in Stdlib.QArith.Qreduction]
Qpower_positive_zero [in Stdlib.micromega.RMicromega]
Qpower_positive_eq_zero [in Stdlib.micromega.RMicromega]
Qpower_2powneg_le_inv [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
Qpower_2_neg_le_one [in Stdlib.Reals.ClassicalDedekindReals]
Qpower_2_invneg_le_pow [in Stdlib.Reals.ClassicalDedekindReals]
Qpower_2_neg_eq_natpow_inv [in Stdlib.Reals.ClassicalDedekindReals]
Qpower_theory [in Stdlib.QArith.Qfield]
Qpower_le_compat_l_inv [in Stdlib.QArith.Qpower]
Qpower_lt_compat_l_inv [in Stdlib.QArith.Qpower]
Qpower_le_compat_l [in Stdlib.QArith.Qpower]
Qpower_lt_compat_l [in Stdlib.QArith.Qpower]
Qpower_decomp_neg_neg [in Stdlib.QArith.Qpower]
Qpower_decomp_neg_pos [in Stdlib.QArith.Qpower]
Qpower_decomp_pos [in Stdlib.QArith.Qpower]
Qpower_mult [in Stdlib.QArith.Qpower]
Qpower_minus_neg [in Stdlib.QArith.Qpower]
Qpower_minus_pos [in Stdlib.QArith.Qpower]
Qpower_minus [in Stdlib.QArith.Qpower]
Qpower_opp [in Stdlib.QArith.Qpower]
Qpower_plus' [in Stdlib.QArith.Qpower]
Qpower_plus [in Stdlib.QArith.Qpower]
Qpower_1_le [in Stdlib.QArith.Qpower]
Qpower_1_le_pos [in Stdlib.QArith.Qpower]
Qpower_1_lt [in Stdlib.QArith.Qpower]
Qpower_1_lt_pos [in Stdlib.QArith.Qpower]
Qpower_0_lt [in Stdlib.QArith.Qpower]
Qpower_0_le [in Stdlib.QArith.Qpower]
Qpower_not_0 [in Stdlib.QArith.Qpower]
Qpower_1_r [in Stdlib.QArith.Qpower]
Qpower_0_r [in Stdlib.QArith.Qpower]
Qpower_1 [in Stdlib.QArith.Qpower]
Qpower_0 [in Stdlib.QArith.Qpower]
Qpower_decomp_positive [in Stdlib.QArith.Qpower]
Qpower_mult_positive [in Stdlib.QArith.Qpower]
Qpower_minus_positive [in Stdlib.QArith.Qpower]
Qpower_plus_positive [in Stdlib.QArith.Qpower]
Qpower_pos_positive [in Stdlib.QArith.Qpower]
Qpower_not_0_positive [in Stdlib.QArith.Qpower]
Qpower_positive_0 [in Stdlib.QArith.Qpower]
Qpower_positive_1 [in Stdlib.QArith.Qpower]
Qpower0 [in Stdlib.micromega.RMicromega]
Qreduce_zero [in Stdlib.QArith.QArith_base]
Qreduce_den_inject_Z_r [in Stdlib.QArith.QArith_base]
Qreduce_den_inject_Z_l [in Stdlib.QArith.QArith_base]
Qreduce_den_r [in Stdlib.QArith.QArith_base]
Qreduce_den_l [in Stdlib.QArith.QArith_base]
Qreduce_num_r [in Stdlib.QArith.QArith_base]
Qreduce_num_l [in Stdlib.QArith.QArith_base]
Qreduce_r [in Stdlib.QArith.QArith_base]
Qreduce_l [in Stdlib.QArith.QArith_base]
Qred_involutive [in Stdlib.QArith.Qcanon]
Qred_iff [in Stdlib.QArith.Qcanon]
Qred_identity2 [in Stdlib.QArith.Qcanon]
Qred_identity [in Stdlib.QArith.Qcanon]
Qred_abs [in Stdlib.QArith.Qcabs]
Qred_lt [in Stdlib.QArith.Qreduction]
Qred_le [in Stdlib.QArith.Qreduction]
Qred_compare [in Stdlib.QArith.Qreduction]
Qred_opp [in Stdlib.QArith.Qreduction]
Qred_eq_iff [in Stdlib.QArith.Qreduction]
Qred_complete [in Stdlib.QArith.Qreduction]
Qred_correct [in Stdlib.QArith.Qreduction]
QReval_formula_compat [in Stdlib.micromega.RMicromega]
Qsor [in Stdlib.micromega.QMicromega]
QSORaddon [in Stdlib.micromega.RMicromega]
QSORaddon [in Stdlib.micromega.QMicromega]
Qsqr_nonneg [in Stdlib.QArith.Qpower]
QTautoChecker_sound [in Stdlib.micromega.QMicromega]
quadruple [in Stdlib.Reals.Ranalysis2]
quadruple_var [in Stdlib.Reals.Ranalysis2]
qualifE [in Stdlib.ssr.ssrbool]
quotient [in Stdlib.Arith.Euclid]
quotient_by_2 [in Stdlib.Numbers.Cyclic.Int63.Uint63]
quots_spec [in Stdlib.micromega.ZifySint63]
QWeakChecker_sound [in Stdlib.micromega.QMicromega]
Q_dec [in Stdlib.QArith.QArith_base]
Q_apart_0_1 [in Stdlib.QArith.QArith_base]
Q_of_RcstR [in Stdlib.micromega.RMicromega]
Q_apart_0_1 [in Stdlib.QArith.Qcanon]
Q_one_zero [in Stdlib.setoid_ring.Rings_Q]
Q_one_zero [in Stdlib.nsatz.NsatzTactic]
Q.plus_min_distr_r [in Stdlib.QArith.Qminmax]
Q.plus_min_distr_l [in Stdlib.QArith.Qminmax]
Q.plus_max_distr_r [in Stdlib.QArith.Qminmax]
Q.plus_max_distr_l [in Stdlib.QArith.Qminmax]
Q2Qc_eq_iff [in Stdlib.QArith.Qcanon]
Q2RpowerRZ [in Stdlib.micromega.RMicromega]
Q2R_pow_N [in Stdlib.micromega.RMicromega]
Q2R_pow_pos [in Stdlib.micromega.RMicromega]
Q2R_inv_ext [in Stdlib.micromega.RMicromega]
Q2R_1 [in Stdlib.micromega.RMicromega]
Q2R_0 [in Stdlib.micromega.RMicromega]
Q2R_div [in Stdlib.QArith.Qreals]
Q2R_inv [in Stdlib.QArith.Qreals]
Q2R_minus [in Stdlib.QArith.Qreals]
Q2R_opp [in Stdlib.QArith.Qreals]
Q2R_mult [in Stdlib.QArith.Qreals]
Q2R_plus [in Stdlib.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 (26071 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 (1003 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 (815 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 (1771 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 (589 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 (961 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 (12021 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 (308 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 (496 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 (906 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 (1204 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 (4844 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)