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 (18816 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)
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 (708 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 (407 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 (8932 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)
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)
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)
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 (203 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 (550 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)
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 (1235 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 (2946 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 (67 entries)

Q (lemma)

Qabs_triangle_reverse [in Qabs_triangle_reverse]
Qabs_pos [in Qabs_pos]
Qabs_neg [in Qabs_neg]
Qabs_nonneg [in Qabs_nonneg]
Qabs_diff_Qle_condition [in Qabs_diff_Qle_condition]
Qabs_opp [in Qabs_opp]
Qabs_case [in Qabs_case]
Qabs_Qle_condition [in Qabs_Qle_condition]
Qabs_Qminus [in Qabs_Qminus]
Qabs_triangle [in Qabs_triangle]
Qabs_Qmult [in Qabs_Qmult]
Qcdiv_mult_l [in Qcdiv_mult_l]
Qceiling_resp_le [in Qceiling_resp_le]
Qceiling_Z [in Qceiling_Z]
Qceiling_lt [in Qceiling_lt]
Qceq_alt [in Qceq_alt]
Qcgt_alt [in Qcgt_alt]
Qcinv_mult_distr [in Qcinv_mult_distr]
Qcle_minus_iff [in Qcle_minus_iff]
Qcle_lt_or_eq [in Qcle_lt_or_eq]
Qcle_not_lt [in Qcle_not_lt]
Qcle_refl [in Qcle_refl]
Qcle_antisym [in Qcle_antisym]
Qcle_lt_trans [in Qcle_lt_trans]
Qcle_trans [in Qcle_trans]
Qclt_le_dec [in Qclt_le_dec]
Qclt_le_weak [in Qclt_le_weak]
Qclt_alt [in Qclt_alt]
Qclt_trans [in Qclt_trans]
Qclt_not_eq [in Qclt_not_eq]
Qclt_le_trans [in Qclt_le_trans]
Qclt_not_le [in Qclt_not_le]
Qclt_minus_iff [in Qclt_minus_iff]
Qcmult_assoc [in Qcmult_assoc]
Qcmult_inv_l [in Qcmult_inv_l]
Qcmult_plus_distr_l [in Qcmult_plus_distr_l]
Qcmult_le_compat_r [in Qcmult_le_compat_r]
Qcmult_integral [in Qcmult_integral]
Qcmult_comm [in Qcmult_comm]
Qcmult_div_r [in Qcmult_div_r]
Qcmult_lt_compat_r [in Qcmult_lt_compat_r]
Qcmult_integral_l [in Qcmult_integral_l]
Qcmult_lt_0_le_reg_r [in Qcmult_lt_0_le_reg_r]
Qcmult_inv_r [in Qcmult_inv_r]
Qcmult_plus_distr_r [in Qcmult_plus_distr_r]
Qcmult_1_r [in Qcmult_1_r]
Qcmult_1_l [in Qcmult_1_l]
Qcnot_lt_le [in Qcnot_lt_le]
Qcnot_le_lt [in Qcnot_le_lt]
Qcompare_antisym [in Qcompare_antisym]
Qcompare_spec [in Qcompare_spec]
Qcopp_involutive [in Qcopp_involutive]
Qcopp_le_compat [in Qcopp_le_compat]
Qcplus_0_r [in Qcplus_0_r]
Qcplus_comm [in Qcplus_comm]
Qcplus_opp_r [in Qcplus_opp_r]
Qcplus_0_l [in Qcplus_0_l]
Qcplus_assoc [in Qcplus_assoc]
Qcplus_le_compat [in Qcplus_le_compat]
Qcpower_1 [in Qcpower_1]
Qcpower_0 [in Qcpower_0]
Qcpower_pos [in Qcpower_pos]
Qc_dec [in Qc_dec]
Qc_is_canon [in Qc_is_canon]
Qc_eq_dec [in Qc_eq_dec]
Qc_decomp [in Qc_decomp]
Qc_eq_bool_correct [in Qc_eq_bool_correct]
Qdiv_power [in Qdiv_power]
Qdiv_mult_l [in Qdiv_mult_l]
Qeq_sym [in Qeq_sym]
Qeq_dec [in Qeq_dec]
Qeq_bool_neq [in Qeq_bool_neq]
Qeq_refl [in Qeq_refl]
Qeq_eq_bool [in Qeq_eq_bool]
Qeq_bool_eq [in Qeq_bool_eq]
Qeq_trans [in Qeq_trans]
Qeq_alt [in Qeq_alt]
Qeq_bool_iff [in Qeq_bool_iff]
Qeq_eqR [in Qeq_eqR]
Qfloor_le [in Qfloor_le]
Qfloor_Z [in Qfloor_Z]
Qfloor_resp_le [in Qfloor_resp_le]
Qge_alt [in Qge_alt]
Qge_alt [in Qge_alt]
Qgt_alt [in Qgt_alt]
Qinv_mult_distr [in Qinv_mult_distr]
Qinv_le_0_compat [in Qinv_le_0_compat]
Qinv_power_n [in Qinv_power_n]
Qinv_involutive [in Qinv_involutive]
Qinv_lt_0_compat [in Qinv_lt_0_compat]
Qinv_power [in Qinv_power]
Qinv_power_positive [in Qinv_power_positive]
Qle_bool_imp_le [in Qle_bool_imp_le]
Qle_shift_div_l [in Qle_shift_div_l]
Qle_trans [in Qle_trans]
Qle_lt_or_eq [in Qle_lt_or_eq]
Qle_not_lt [in Qle_not_lt]
Qle_lt_trans [in Qle_lt_trans]
Qle_minus_iff [in Qle_minus_iff]
Qle_floor_ceiling [in Qle_floor_ceiling]
Qle_shift_inv_l [in Qle_shift_inv_l]
Qle_Qabs [in Qle_Qabs]
Qle_bool_iff [in Qle_bool_iff]
Qle_shift_inv_r [in Qle_shift_inv_r]
Qle_ceiling [in Qle_ceiling]
Qle_Rle [in Qle_Rle]
Qle_antisym [in Qle_antisym]
Qle_shift_div_r [in Qle_shift_div_r]
Qle_lteq [in Qle_lteq]
Qle_alt [in Qle_alt]
Qle_alt [in Qle_alt]
Qle_refl [in Qle_refl]
Qlt_floor [in Qlt_floor]
Qlt_le_trans [in Qlt_le_trans]
Qlt_alt [in Qlt_alt]
Qlt_shift_div_r [in Qlt_shift_div_r]
Qlt_le_dec [in Qlt_le_dec]
Qlt_trans [in Qlt_trans]
Qlt_irrefl [in Qlt_irrefl]
Qlt_shift_div_l [in Qlt_shift_div_l]
Qlt_minus_iff [in Qlt_minus_iff]
Qlt_Rlt [in Qlt_Rlt]
Qlt_shift_inv_l [in Qlt_shift_inv_l]
Qlt_shift_inv_r [in Qlt_shift_inv_r]
Qlt_not_le [in Qlt_not_le]
Qlt_le_weak [in Qlt_le_weak]
Qlt_not_eq [in Qlt_not_eq]
Qmake_Qdiv [in Qmake_Qdiv]
Qminus'_correct [in Qminus'_correct]
Qmult_inv_r [in Qmult_inv_r]
Qmult_inj_r [in Qmult_inj_r]
Qmult_lt_0_le_reg_r [in Qmult_lt_0_le_reg_r]
Qmult_power [in Qmult_power]
Qmult_le_r [in Qmult_le_r]
Qmult_power_positive [in Qmult_power_positive]
Qmult_plus_distr_l [in Qmult_plus_distr_l]
Qmult_le_compat_r [in Qmult_le_compat_r]
Qmult_lt_compat_r [in Qmult_lt_compat_r]
Qmult_le_0_compat [in Qmult_le_0_compat]
Qmult_0_l [in Qmult_0_l]
Qmult_lt_l [in Qmult_lt_l]
Qmult_plus_distr_r [in Qmult_plus_distr_r]
Qmult_assoc [in Qmult_assoc]
Qmult_1_r [in Qmult_1_r]
Qmult_lt_r [in Qmult_lt_r]
Qmult_integral [in Qmult_integral]
Qmult_0_r [in Qmult_0_r]
Qmult_div_r [in Qmult_div_r]
Qmult_comm [in Qmult_comm]
Qmult_inj_l [in Qmult_inj_l]
Qmult_integral_l [in Qmult_integral_l]
Qmult_1_l [in Qmult_1_l]
Qmult_le_l [in Qmult_le_l]
Qmult'_correct [in Qmult'_correct]
Qnot_lt_le [in Qnot_lt_le]
Qnot_eq_sym [in Qnot_eq_sym]
Qnot_le_lt [in Qnot_le_lt]
Qopp_involutive [in Qopp_involutive]
Qopp_plus [in Qopp_plus]
Qopp_lt_compat [in Qopp_lt_compat]
Qopp_le_compat [in Qopp_le_compat]
Qopp_opp [in Qopp_opp]
Qplus_lt_r [in Qplus_lt_r]
Qplus_comm [in Qplus_comm]
Qplus_lt_le_compat [in Qplus_lt_le_compat]
Qplus_le_r [in Qplus_le_r]
Qplus_le_compat [in Qplus_le_compat]
Qplus_0_l [in Qplus_0_l]
Qplus_inj_l [in Qplus_inj_l]
Qplus_inj_r [in Qplus_inj_r]
Qplus_lt_l [in Qplus_lt_l]
Qplus_opp_r [in Qplus_opp_r]
Qplus_0_r [in Qplus_0_r]
Qplus_le_l [in Qplus_le_l]
Qplus_assoc [in Qplus_assoc]
Qplus'_correct [in Qplus'_correct]
Qpower_minus_positive [in Qpower_minus_positive]
Qpower_0 [in Qpower_0]
Qpower_positive_0 [in Qpower_positive_0]
Qpower_pos_positive [in Qpower_pos_positive]
Qpower_mult [in Qpower_mult]
Qpower_not_0_positive [in Qpower_not_0_positive]
Qpower_1 [in Qpower_1]
Qpower_plus [in Qpower_plus]
Qpower_opp [in Qpower_opp]
Qpower_plus' [in Qpower_plus']
Qpower_positive_1 [in Qpower_positive_1]
Qpower_decomp [in Qpower_decomp]
Qpower_plus_positive [in Qpower_plus_positive]
Qpower_theory [in Qpower_theory]
Qpower_mult_positive [in Qpower_mult_positive]
Qpower_pos [in Qpower_pos]
QProperties.add_opp_diag_r [in add_opp_diag_r]
QProperties.add_assoc [in add_assoc]
QProperties.add_comm [in add_comm]
QProperties.add_0_l [in add_0_l]
QProperties.compare_spec [in compare_spec]
QProperties.div_mul_inv [in div_mul_inv]
QProperties.eqb_complete [in eqb_complete]
QProperties.eqb_eq [in eqb_eq]
QProperties.eqb_correct [in eqb_correct]
QProperties.le_lteq [in le_lteq]
QProperties.lt_total [in lt_total]
QProperties.max_r [in max_r]
QProperties.max_l [in max_l]
QProperties.min_r [in min_r]
QProperties.min_l [in min_l]
QProperties.mul_inv_diag_l [in mul_inv_diag_l]
QProperties.mul_1_l [in mul_1_l]
QProperties.mul_add_distr_r [in mul_add_distr_r]
QProperties.mul_comm [in mul_comm]
QProperties.mul_assoc [in mul_assoc]
QProperties.neq_1_0 [in neq_1_0]
QProperties.sub_add_opp [in sub_add_opp]
Qred_compare [in Qred_compare]
Qred_complete [in Qred_complete]
Qred_identity [in Qred_identity]
Qred_identity2 [in Qred_identity2]
Qred_opp [in Qred_opp]
Qred_involutive [in Qred_involutive]
Qred_correct [in Qred_correct]
Qred_iff [in Qred_iff]
Qsqr_nonneg [in Qsqr_nonneg]
quadruple [in quadruple]
quadruple_var [in quadruple_var]
quotient [in quotient]
quotient_by_2 [in quotient_by_2]
Q_apart_0_1 [in Q_apart_0_1]
Q_apart_0_1 [in Q_apart_0_1]
Q_dec [in Q_dec]
Q.plus_max_distr_l [in plus_max_distr_l]
Q.plus_max_distr_r [in plus_max_distr_r]
Q.plus_min_distr_l [in plus_min_distr_l]
Q.plus_min_distr_r [in plus_min_distr_r]
Q2R_inv [in Q2R_inv]
Q2R_div [in Q2R_div]
Q2R_opp [in Q2R_opp]
Q2R_mult [in Q2R_mult]
Q2R_minus [in Q2R_minus]
Q2R_plus [in Q2R_plus]



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 (18816 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)
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 (708 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 (407 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 (8932 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)
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)
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)
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 (203 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 (550 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)
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 (1235 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 (2946 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 (67 entries)