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)

R

R [definition, in R]
R [module, in R]
R [axiom, in R]
R [definition, in R]
Rabs [definition, in Rabs]
Rabs_triang_gen [lemma, in Rabs_triang_gen]
Rabs_derive_2 [lemma, in Rabs_derive_2]
Rabs_pos_lt [lemma, in Rabs_pos_lt]
Rabs_Rabsolu [lemma, in Rabs_Rabsolu]
Rabs_def2 [lemma, in Rabs_def2]
Rabs_triang_inv2 [lemma, in Rabs_triang_inv2]
Rabs_pos [lemma, in Rabs_pos]
Rabs_def1 [lemma, in Rabs_def1]
Rabs_left1 [lemma, in Rabs_left1]
Rabs_right [lemma, in Rabs_right]
Rabs_4 [lemma, in Rabs_4]
Rabs_R1 [lemma, in Rabs_R1]
Rabs_no_R0 [lemma, in Rabs_no_R0]
Rabs_pos_eq [lemma, in Rabs_pos_eq]
Rabs_minus_sym [lemma, in Rabs_minus_sym]
Rabs_R0 [lemma, in Rabs_R0]
Rabs_mult [lemma, in Rabs_mult]
Rabs_derive_1 [lemma, in Rabs_derive_1]
Rabs_triang [lemma, in Rabs_triang]
Rabs_Zabs [lemma, in Rabs_Zabs]
Rabs_Rinv [lemma, in Rabs_Rinv]
Rabs_triang_inv [lemma, in Rabs_triang_inv]
Rabs_Ropp [lemma, in Rabs_Ropp]
Rabs_left [lemma, in Rabs_left]
rad_deg [lemma, in rad_deg]
Ranalysis [library]
Ranalysis_reg [library]
Ranalysis1 [library]
Ranalysis2 [library]
Ranalysis3 [library]
Ranalysis4 [library]
Ranalysis5 [library]
Ratan [library]
Ratan_CVU' [lemma, in Ratan_CVU']
Ratan_is_ps_atan [lemma, in Ratan_is_ps_atan]
Ratan_seq_decreasing [lemma, in Ratan_seq_decreasing]
Ratan_seq_opp [lemma, in Ratan_seq_opp]
Ratan_seq_converging [lemma, in Ratan_seq_converging]
Ratan_seq [definition, in Ratan_seq]
Ratan_CVU [lemma, in Ratan_CVU]
Raw [module, in Raw]
Raw [module, in Raw]
Raw [module, in Raw]
RawSets [module, in RawSets]
RawSets.choose_spec3 [axiom, in choose_spec3]
RawSets.compare_spec [axiom, in compare_spec]
RawSets.elements_spec2 [axiom, in elements_spec2]
RawSets.max_elt_spec3 [axiom, in max_elt_spec3]
RawSets.max_elt_spec2 [axiom, in max_elt_spec2]
RawSets.max_elt_spec1 [axiom, in max_elt_spec1]
RawSets.min_elt_spec2 [axiom, in min_elt_spec2]
RawSets.min_elt_spec3 [axiom, in min_elt_spec3]
RawSets.min_elt_spec1 [axiom, in min_elt_spec1]
RawSets.Spec [section, in Spec]
RawSets.Spec.s [variable, in s]
RawSets.Spec.s' [variable, in s']
RawSets.Spec.x [variable, in x]
RawSets.Spec.y [variable, in y]
Raw.add [definition, in add]
Raw.add_Inf [lemma, in add_Inf]
Raw.add_1 [lemma, in add_1]
Raw.add_1 [lemma, in add_1]
Raw.add_eq [lemma, in add_eq]
Raw.add_sorted [lemma, in add_sorted]
Raw.add_3' [lemma, in add_3']
Raw.add_NoDup [lemma, in add_NoDup]
Raw.add_2 [lemma, in add_2]
Raw.add_2 [lemma, in add_2]
Raw.add_not_eq [lemma, in add_not_eq]
Raw.add_3 [lemma, in add_3]
Raw.add_3 [lemma, in add_3]
Raw.assert_false [definition, in assert_false]
Raw.at_least_left [definition, in at_least_left]
Raw.at_least_one_then_f [definition, in at_least_one_then_f]
Raw.at_least_one_then_f [definition, in at_least_one_then_f]
Raw.at_least_one [definition, in at_least_one]
Raw.at_least_one [definition, in at_least_one]
Raw.at_least_right [definition, in at_least_right]
Raw.bal [definition, in bal]
Raw.BSLeaf [constructor, in BSLeaf]
Raw.BSNode [constructor, in BSNode]
Raw.bst [inductive, in bst]
Raw.cardinal [definition, in cardinal]
Raw.check [definition, in check]
Raw.combine [definition, in combine]
Raw.combine [definition, in combine]
Raw.combine_lelistA [lemma, in combine_lelistA]
Raw.combine_l_1 [lemma, in combine_l_1]
Raw.combine_r [definition, in combine_r]
Raw.combine_l [definition, in combine_l]
Raw.combine_r_1 [lemma, in combine_r_1]
Raw.combine_1 [lemma, in combine_1]
Raw.combine_1 [lemma, in combine_1]
Raw.combine_sorted [lemma, in combine_sorted]
Raw.combine_NoDup [lemma, in combine_NoDup]
Raw.concat [definition, in concat]
Raw.cons [definition, in cons]
Raw.create [definition, in create]
Raw.elements [definition, in elements]
Raw.elements [definition, in elements]
Raw.elements [definition, in elements]
Raw.elements_3w [lemma, in elements_3w]
Raw.elements_3w [lemma, in elements_3w]
Raw.elements_aux [definition, in elements_aux]
Raw.elements_3 [lemma, in elements_3]
Raw.elements_1 [lemma, in elements_1]
Raw.elements_1 [lemma, in elements_1]
Raw.elements_2 [lemma, in elements_2]
Raw.elements_2 [lemma, in elements_2]
Raw.Elt [section, in Elt]
Raw.Elt [section, in Elt]
Raw.Elt [section, in Elt]
Raw.Elt.cmp [variable, in cmp]
Raw.Elt.elt [variable, in elt]
Raw.Elt.elt [variable, in elt]
Raw.Elt.elt [variable, in elt]
Raw.Elt.elt' [variable, in elt']
Raw.Elt.elt' [variable, in elt']
<< _ , _ , _ >> [notation, in ::'<<'_x_','_x_','_x_'>>']
Raw.Elt2 [section, in Elt2]
Raw.Elt2 [section, in Elt2]
Raw.Elt2.elt [variable, in elt]
Raw.Elt2.elt [variable, in elt]
Raw.Elt2.elt' [variable, in elt']
Raw.Elt2.elt' [variable, in elt']
Raw.Elt3 [section, in Elt3]
Raw.Elt3 [section, in Elt3]
Raw.Elt3.elt [variable, in elt]
Raw.Elt3.elt [variable, in elt]
Raw.Elt3.elt' [variable, in elt']
Raw.Elt3.elt' [variable, in elt']
Raw.Elt3.elt'' [variable, in elt'']
Raw.Elt3.elt'' [variable, in elt'']
Raw.Elt3.f [variable, in f]
Raw.Elt3.f [variable, in f]
Raw.empty [definition, in empty]
Raw.empty [definition, in empty]
Raw.empty [definition, in empty]
Raw.Empty [definition, in Empty]
Raw.Empty [definition, in Empty]
Raw.empty_sorted [lemma, in empty_sorted]
Raw.empty_NoDup [lemma, in empty_NoDup]
Raw.empty_1 [lemma, in empty_1]
Raw.empty_1 [lemma, in empty_1]
Raw.End [constructor, in End]
Raw.enumeration [inductive, in enumeration]
Raw.eqk [abbreviation, in eqk]
Raw.eqk [abbreviation, in eqk]
Raw.eqke [abbreviation, in eqke]
Raw.eqke [abbreviation, in eqke]
Raw.equal [definition, in equal]
Raw.equal [definition, in equal]
Raw.equal_cons [lemma, in equal_cons]
Raw.equal_cont [definition, in equal_cont]
Raw.equal_2 [lemma, in equal_2]
Raw.equal_2 [lemma, in equal_2]
Raw.equal_1 [lemma, in equal_1]
Raw.equal_1 [lemma, in equal_1]
Raw.equal_end [definition, in equal_end]
Raw.equal_more [definition, in equal_more]
Raw.Equivb [definition, in Equivb]
Raw.Equivb [definition, in Equivb]
Raw.find [definition, in find]
Raw.find_eq [lemma, in find_eq]
Raw.find_2 [lemma, in find_2]
Raw.find_2 [lemma, in find_2]
Raw.find_1 [lemma, in find_1]
Raw.find_1 [lemma, in find_1]
Raw.fold [definition, in fold]
Raw.fold_right_pair [definition, in fold_right_pair]
Raw.fold_right_pair [definition, in fold_right_pair]
Raw.fold_right_pair_NoDup [lemma, in fold_right_pair_NoDup]
Raw.fold_1 [lemma, in fold_1]
Raw.fold_1 [lemma, in fold_1]
Raw.gt_tree [definition, in gt_tree]
Raw.height [definition, in height]
Raw.In [abbreviation, in In]
Raw.In [abbreviation, in In]
Raw.In [inductive, in In]
Raw.Inf [abbreviation, in Inf]
Raw.InLeft [constructor, in InLeft]
Raw.InRight [constructor, in InRight]
Raw.InRoot [constructor, in InRoot]
Raw.Invariants [section, in Invariants]
Raw.Invariants.elt [variable, in elt]
Raw.In0 [definition, in In0]
Raw.is_empty_1 [lemma, in is_empty_1]
Raw.is_empty_1 [lemma, in is_empty_1]
Raw.is_empty [definition, in is_empty]
Raw.is_empty [definition, in is_empty]
Raw.is_empty [definition, in is_empty]
Raw.is_empty_2 [lemma, in is_empty_2]
Raw.is_empty_2 [lemma, in is_empty_2]
Raw.join [definition, in join]
Raw.key [definition, in key]
Raw.key [definition, in key]
Raw.key [definition, in key]
Raw.Leaf [constructor, in Leaf]
Raw.ltk [abbreviation, in ltk]
Raw.lt_tree [definition, in lt_tree]
Raw.map [definition, in map]
Raw.map [definition, in map]
Raw.map [definition, in map]
Raw.mapi [definition, in mapi]
Raw.mapi [definition, in mapi]
Raw.mapi [definition, in mapi]
Raw.mapi_NoDup [lemma, in mapi_NoDup]
Raw.mapi_2 [lemma, in mapi_2]
Raw.mapi_2 [lemma, in mapi_2]
Raw.mapi_sorted [lemma, in mapi_sorted]
Raw.mapi_1 [lemma, in mapi_1]
Raw.mapi_1 [lemma, in mapi_1]
Raw.mapi_lelistA [lemma, in mapi_lelistA]
Raw.MapsLeft [constructor, in MapsLeft]
Raw.MapsRight [constructor, in MapsRight]
Raw.MapsRoot [constructor, in MapsRoot]
Raw.MapsTo [abbreviation, in MapsTo]
Raw.MapsTo [abbreviation, in MapsTo]
Raw.MapsTo [inductive, in MapsTo]
Raw.map_1 [lemma, in map_1]
Raw.map_1 [lemma, in map_1]
Raw.map_option [definition, in map_option]
Raw.map_lelistA [lemma, in map_lelistA]
Raw.map_sorted [lemma, in map_sorted]
Raw.map_2 [lemma, in map_2]
Raw.map_2 [lemma, in map_2]
Raw.map_NoDup [lemma, in map_NoDup]
Raw.Map2 [section, in Map2]
Raw.map2 [definition, in map2]
Raw.map2 [definition, in map2]
Raw.map2 [definition, in map2]
Raw.map2_alt_equiv [lemma, in map2_alt_equiv]
Raw.map2_r [definition, in map2_r]
Raw.Map2_opt [section, in Map2_opt]
Raw.map2_opt [definition, in map2_opt]
Raw.Map2_opt.elt' [variable, in elt']
Raw.map2_sorted [lemma, in map2_sorted]
Raw.Map2_opt.f [variable, in f]
Raw.Map2_opt.elt [variable, in elt]
Raw.map2_2 [lemma, in map2_2]
Raw.map2_2 [lemma, in map2_2]
Raw.map2_NoDup [lemma, in map2_NoDup]
Raw.Map2_opt.mapl [variable, in mapl]
Raw.map2_0 [lemma, in map2_0]
Raw.map2_0 [lemma, in map2_0]
Raw.map2_1 [lemma, in map2_1]
Raw.map2_1 [lemma, in map2_1]
Raw.Map2_opt.elt'' [variable, in elt'']
Raw.map2_alt [definition, in map2_alt]
Raw.map2_l [definition, in map2_l]
Raw.Map2_opt.mapr [variable, in mapr]
Raw.Map2.elt [variable, in elt]
Raw.Map2.elt' [variable, in elt']
Raw.Map2.elt'' [variable, in elt'']
Raw.Map2.f [variable, in f]
Raw.mem [definition, in mem]
Raw.mem_1 [lemma, in mem_1]
Raw.mem_1 [lemma, in mem_1]
Raw.mem_2 [lemma, in mem_2]
Raw.mem_2 [lemma, in mem_2]
Raw.merge [definition, in merge]
Raw.mktriple [constructor, in mktriple]
Raw.More [constructor, in More]
Raw.MX [module, in Raw.MX]
Raw.Node [constructor, in Node]
Raw.NoDupA [abbreviation, in NoDupA]
Raw.oee' [abbreviation, in oee']
Raw.oee' [abbreviation, in oee']
Raw.option_cons [definition, in option_cons]
Raw.option_cons [definition, in option_cons]
Raw.Proofs [module, in Raw.Proofs]
Raw.Proofs.L [module, in Raw.Proofs.L]
Raw.Proofs.MX [module, in Raw.Proofs.MX]
Raw.Proofs.PX [module, in Raw.Proofs.PX]
Raw.PX [module, in Raw.PX]
Raw.PX [module, in Raw.PX]
Raw.remove [definition, in remove]
Raw.remove_3' [lemma, in remove_3']
Raw.remove_sorted [lemma, in remove_sorted]
Raw.remove_NoDup [lemma, in remove_NoDup]
Raw.remove_2 [lemma, in remove_2]
Raw.remove_2 [lemma, in remove_2]
Raw.remove_1 [lemma, in remove_1]
Raw.remove_1 [lemma, in remove_1]
Raw.remove_3 [lemma, in remove_3]
Raw.remove_3 [lemma, in remove_3]
Raw.remove_Inf [lemma, in remove_Inf]
Raw.remove_min [definition, in remove_min]
Raw.Sort [abbreviation, in Sort]
Raw.split [definition, in split]
Raw.Submap [definition, in Submap]
Raw.submap [definition, in submap]
Raw.submap_2 [lemma, in submap_2]
Raw.submap_1 [lemma, in submap_1]
Raw.t [definition, in t]
Raw.t [definition, in t]
Raw.t [abbreviation, in t]
Raw.t [abbreviation, in t]
Raw.tree [inductive, in tree]
Raw.triple [record, in triple]
Raw.t_opt [projection, in t_opt]
Raw.t_right [projection, in t_right]
Raw.t_left [projection, in t_left]
_ #l [notation, in ::x_'#l']
_ #r [notation, in ::x_'#r']
_ #o [notation, in ::x_'#o']
<< _ , _ , _ >> [notation, in ::'<<'_x_','_x_','_x_'>>']
Raw2Sets [module, in Raw2Sets]
Raw2SetsOn [module, in Raw2SetsOn]
Raw2SetsOn.choose_spec3 [lemma, in choose_spec3]
Raw2SetsOn.compare [definition, in compare]
Raw2SetsOn.compare_spec [lemma, in compare_spec]
Raw2SetsOn.elements_spec2 [lemma, in elements_spec2]
Raw2SetsOn.lt [definition, in lt]
Raw2SetsOn.lt_compat [instance, in lt_compat]
Raw2SetsOn.lt_strorder [instance, in lt_strorder]
Raw2SetsOn.max_elt_spec3 [lemma, in max_elt_spec3]
Raw2SetsOn.max_elt_spec2 [lemma, in max_elt_spec2]
Raw2SetsOn.max_elt [definition, in max_elt]
Raw2SetsOn.max_elt_spec1 [lemma, in max_elt_spec1]
Raw2SetsOn.min_elt_spec2 [lemma, in min_elt_spec2]
Raw2SetsOn.min_elt_spec3 [lemma, in min_elt_spec3]
Raw2SetsOn.min_elt_spec1 [lemma, in min_elt_spec1]
Raw2SetsOn.min_elt [definition, in min_elt]
Raw2SetsOn.Spec [section, in Spec]
Raw2SetsOn.Spec.s [variable, in s]
Raw2SetsOn.Spec.s' [variable, in s']
Raw2SetsOn.Spec.s'' [variable, in s'']
Raw2SetsOn.Spec.x [variable, in x]
Raw2SetsOn.Spec.y [variable, in y]
Raw2Sets.E [module, in Raw2Sets.E]
Raxioms [library]
Rbase [library]
Rbasic_fun [library]
Rcase_abs [lemma, in Rcase_abs]
Rcompare [definition, in Rcompare]
Rcompare_spec [lemma, in Rcompare_spec]
Rcomplete [library]
Rcontinuity_abs [lemma, in Rcontinuity_abs]
Rdefinitions [library]
Rderiv [library]
Rderivable_pt_abs [lemma, in Rderivable_pt_abs]
Rdichotomy [lemma, in Rdichotomy]
Rdiv [definition, in Rdiv]
Reals [library]
recl [definition, in recl]
recl_aux [definition, in recl_aux]
recr [definition, in recr]
recrbis [definition, in recrbis]
recrbis_aux_equiv [lemma, in recrbis_aux_equiv]
recrbis_aux [definition, in recrbis_aux]
recrbis_equiv [lemma, in recrbis_equiv]
recr_aux_converges [lemma, in recr_aux_converges]
recr_aux [definition, in recr_aux]
recr_eqn [lemma, in recr_eqn]
recr_aux_eqn [lemma, in recr_aux_eqn]
rectS [definition, in rectS]
rectS [definition, in rectS]
rect2 [definition, in rect2]
rect2 [definition, in rect2]
Red [constructor, in Red]
Reduce [section, in Reduce]
ReduceRec [section, in ReduceRec]
ReduceRec.c [variable, in c]
ReduceRec.nT [variable, in nT]
ReduceRec.N0 [variable, in N0]
ReduceRec.reduce_1n [variable, in reduce_1n]
ReduceRec.w [variable, in w]
reduce_n1 [definition, in reduce_n1]
reduce_n [definition, in reduce_n]
Reduce.eq0 [variable, in eq0]
Reduce.nT [variable, in nT]
Reduce.N0 [variable, in N0]
Reduce.reduce_n [variable, in reduce_n]
Reduce.w [variable, in w]
Reduce.zn2z_to_Nt [variable, in zn2z_to_Nt]
ReDun [section, in ReDun]
ReDun.A [variable, in A]
reflect [inductive, in reflect]
ReflectF [constructor, in ReflectF]
ReflectT [constructor, in ReflectT]
reflect_dec [lemma, in reflect_dec]
reflect_iff [lemma, in reflect_iff]
reflexive [definition, in reflexive]
Reflexive [record, in Reflexive]
Reflexive [inductive, in Reflexive]
Reflexive [definition, in Reflexive]
Reflexive_complement_Irreflexive [definition, in Reflexive_complement_Irreflexive]
reflexive_proper [lemma, in reflexive_proper]
Reflexive_Symmetric_Transitive_Closure.R [variable, in R]
Reflexive_Transitive_Closure.R [variable, in R]
Reflexive_Symmetric_Transitive_Closure [section, in Reflexive_Symmetric_Transitive_Closure]
Reflexive_Transitive_Closure [section, in Reflexive_Transitive_Closure]
reflexive_proper_proxy [lemma, in reflexive_proper_proxy]
Reflexive_Symmetric_Transitive_Closure.A [variable, in A]
Reflexive_Transitive_Closure.A [variable, in A]
Reflexive_partial_app_morphism [lemma, in Reflexive_partial_app_morphism]
reflexive_eq_dom_reflexive [instance, in reflexive_eq_dom_reflexive]
reflexivity [projection, in reflexivity]
reflexivity [constructor, in reflexivity]
refl_id [abbreviation, in refl_id]
refl_equal [abbreviation, in refl_equal]
Rel [definition, in Rel]
relation [definition, in relation]
Relation [definition, in Relation]
RelationalChoice [abbreviation, in RelationalChoice]
RelationalChoice [library]
RelationalChoice_on [definition, in RelationalChoice_on]
relational_choice [axiom, in relational_choice]
RelationClasses [library]
RelationPairs [library]
Relations [library]
Relations_3.U [variable, in U]
Relations_2.U [variable, in U]
Relations_1.U [variable, in U]
Relations_3.R [variable, in R]
Relations_2.R [variable, in R]
Relations_1.R [variable, in R]
Relations_1 [section, in Relations_1]
Relations_3 [section, in Relations_3]
Relations_2 [section, in Relations_2]
Relations_2 [library]
Relations_1 [library]
Relations_3_facts [library]
Relations_3 [library]
Relations_1_facts [library]
Relations_2_facts [library]
Relation_Definition.Relations_of_Relations [section, in Relations_of_Relations]
relation_implication_preorder [instance, in relation_implication_preorder]
relation_disjunction_morphism [instance, in relation_disjunction_morphism]
relation_conjunction [definition, in relation_conjunction]
relation_disjunction [definition, in relation_disjunction]
relation_equivalence [definition, in relation_equivalence]
Relation_Definition.Sets_of_Relations [section, in Sets_of_Relations]
Relation_Definition.R [variable, in R]
relation_equivalence_equivalence [instance, in relation_equivalence_equivalence]
Relation_Definition.General_Properties_of_Relations [section, in General_Properties_of_Relations]
Relation_Definition.A [variable, in A]
relation_equivalence_pointwise [instance, in relation_equivalence_pointwise]
Relation_Definition [section, in Relation_Definition]
relation_conjunction_morphism [instance, in relation_conjunction_morphism]
Relation_Definitions [library]
Relation_Operators [library]
relative_non_contradiction_of_definite_descr [lemma, in relative_non_contradiction_of_definite_descr]
relative_non_contradiction_of_indefinite_descr [lemma, in relative_non_contradiction_of_indefinite_descr]
RelCompFun [definition, in RelCompFun]
RelCompFun_Equivalence [instance, in RelCompFun_Equivalence]
RelCompFun_Symmetric [instance, in RelCompFun_Symmetric]
RelCompFun_Irreflexive [instance, in RelCompFun_Irreflexive]
RelCompFun_Reflexive [instance, in RelCompFun_Reflexive]
RelCompFun_StrictOrder [instance, in RelCompFun_StrictOrder]
RelCompFun_compat [instance, in RelCompFun_compat]
RelCompFun_Instances [section, in RelCompFun_Instances]
RelCompFun_Transitive [instance, in RelCompFun_Transitive]
RelProd [definition, in RelProd]
RelProd_Reflexive [instance, in RelProd_Reflexive]
RelProd_Symmetric [instance, in RelProd_Symmetric]
RelProd_Equivalence [instance, in RelProd_Equivalence]
RelProd_Transitive [instance, in RelProd_Transitive]
rel_prime_dec [definition, in rel_prime_dec]
rel_prime_bezout [lemma, in rel_prime_bezout]
rel_prime_mod [lemma, in rel_prime_mod]
rel_choice_and_proof_irrel_imp_guarded_rel_choice [lemma, in rel_choice_and_proof_irrel_imp_guarded_rel_choice]
rel_prime [definition, in rel_prime]
rel_choice_indep_of_general_premises_imp_guarded_rel_choice [lemma, in rel_choice_indep_of_general_premises_imp_guarded_rel_choice]
rel_prime_le_prime [lemma, in rel_prime_le_prime]
rel_prime_sym [lemma, in rel_prime_sym]
rel_prime_1 [lemma, in rel_prime_1]
rel_prime_cross_prod [lemma, in rel_prime_cross_prod]
Rel_of [projection, in Rel_of]
rel_prime_mod_rev [lemma, in rel_prime_mod_rev]
rel_prime_mult [lemma, in rel_prime_mult]
rel_prime_div [lemma, in rel_prime_div]
rel_prime_Zpower_r [lemma, in rel_prime_Zpower_r]
rel_prime_Zpower [lemma, in rel_prime_Zpower]
Remainder [definition, in Remainder]
Remainder [abbreviation, in Remainder]
Remainder [definition, in Remainder]
Remainder_alt [definition, in Remainder_alt]
Remainder_alt [abbreviation, in Remainder_alt]
Remainder_alt [definition, in Remainder_alt]
Remainder_equiv [lemma, in Remainder_equiv]
Remainder_equiv [abbreviation, in Remainder_equiv]
Remainder_equiv [lemma, in Remainder_equiv]
remove [definition, in remove]
removeA [definition, in removeA]
removeA_InA [lemma, in removeA_InA]
removeA_NoDupA [lemma, in removeA_NoDupA]
removeA_equivlistA [lemma, in removeA_equivlistA]
removeA_filter [lemma, in removeA_filter]
removelast [definition, in removelast]
removelast_app [lemma, in removelast_app]
removelast_firstn [lemma, in removelast_firstn]
remove_In [lemma, in remove_In]
replace [definition, in replace]
replace_order [definition, in replace_order]
Reqb [definition, in Reqb]
Reqb_eq [lemma, in Reqb_eq]
Req_ge [lemma, in Req_ge]
Req_ge_sym [lemma, in Req_ge_sym]
Req_le [lemma, in Req_le]
Req_dec [lemma, in Req_dec]
Req_dec [lemma, in Req_dec]
Req_EM_T [lemma, in Req_EM_T]
Req_le_sym [lemma, in Req_le_sym]
respectful [definition, in respectful]
respectful_morphism [instance, in respectful_morphism]
respectful_hetero [definition, in respectful_hetero]
respectful_per [instance, in respectful_per]
respecting [definition, in respecting]
Respecting [section, in Respecting]
respecting_equiv [instance, in respecting_equiv]
Reste [definition, in Reste]
Reste_E_cv [lemma, in Reste_E_cv]
Reste_E [definition, in Reste_E]
Reste_E_maj [lemma, in Reste_E_maj]
reste_cv_R0 [lemma, in reste_cv_R0]
Reste1 [definition, in Reste1]
reste1_maj [lemma, in reste1_maj]
reste1_cv_R0 [lemma, in reste1_cv_R0]
Reste2 [definition, in Reste2]
reste2_maj [lemma, in reste2_maj]
reste2_cv_R0 [lemma, in reste2_cv_R0]
restriction_family [lemma, in restriction_family]
retract [record, in retract]
retract [record, in retract]
retract_pow_U_U [lemma, in retract_pow_U_U]
retract_cond [record, in retract_cond]
rev [definition, in rev]
rev [definition, in rev]
rev_ind [lemma, in rev_ind]
rev_acc [abbreviation, in rev_acc]
rev_append_tail [definition, in rev_append_tail]
rev_unit [lemma, in rev_unit]
rev_alt [lemma, in rev_alt]
rev_eqlistA_compat [instance, in rev_eqlistA_compat]
rev_append_rev [lemma, in rev_append_rev]
rev_nth [lemma, in rev_nth]
rev_length [lemma, in rev_length]
rev_app_distr [lemma, in rev_app_distr]
rev_acc_rev [abbreviation, in rev_acc_rev]
rev_involutive [lemma, in rev_involutive]
rev_append [definition, in rev_append]
rev_append [definition, in rev_append]
rev_list_ind [lemma, in rev_list_ind]
rev' [definition, in rev']
RewriteRelation [record, in RewriteRelation]
RfactN_fact2N_factk [lemma, in RfactN_fact2N_factk]
Rfunctions [library]
Rge [definition, in Rge]
Rgeom [library]
Rge_trans [lemma, in Rge_trans]
Rge_dec [lemma, in Rge_dec]
Rge_ge_eq [lemma, in Rge_ge_eq]
Rge_not_gt [lemma, in Rge_not_gt]
Rge_gt_dec [lemma, in Rge_gt_dec]
Rge_minus [lemma, in Rge_minus]
Rge_le [lemma, in Rge_le]
Rge_gt_trans [lemma, in Rge_gt_trans]
Rge_refl [lemma, in Rge_refl]
Rge_antisym [lemma, in Rge_antisym]
Rge_not_lt [lemma, in Rge_not_lt]
Rge_or_gt [lemma, in Rge_or_gt]
Rgt [definition, in Rgt]
Rgt_not_le [lemma, in Rgt_not_le]
Rgt_or_ge [lemma, in Rgt_or_ge]
Rgt_irrefl [lemma, in Rgt_irrefl]
Rgt_not_ge [lemma, in Rgt_not_ge]
Rgt_ge_trans [lemma, in Rgt_ge_trans]
Rgt_minus [lemma, in Rgt_minus]
Rgt_3PI2_0 [lemma, in Rgt_3PI2_0]
Rgt_2PI_0 [lemma, in Rgt_2PI_0]
Rgt_ge_dec [lemma, in Rgt_ge_dec]
Rgt_lt [lemma, in Rgt_lt]
Rgt_trans [lemma, in Rgt_trans]
Rgt_not_eq [lemma, in Rgt_not_eq]
Rgt_dec [lemma, in Rgt_dec]
Rgt_asym [lemma, in Rgt_asym]
Rgt_eq_compat [lemma, in Rgt_eq_compat]
Rgt_ge [lemma, in Rgt_ge]
RHasMinMax [module, in RHasMinMax]
RHasMinMax.max [definition, in max]
RHasMinMax.max_r [definition, in max_r]
RHasMinMax.max_l [definition, in max_l]
RHasMinMax.min [definition, in min]
RHasMinMax.min_r [definition, in min_r]
RHasMinMax.min_l [definition, in min_l]
RiemannInt [definition, in RiemannInt]
RiemannInt [library]
RiemannInt_P20 [lemma, in RiemannInt_P20]
RiemannInt_P25 [lemma, in RiemannInt_P25]
RiemannInt_P33 [lemma, in RiemannInt_P33]
RiemannInt_P6 [lemma, in RiemannInt_P6]
RiemannInt_P31 [lemma, in RiemannInt_P31]
RiemannInt_P16 [lemma, in RiemannInt_P16]
RiemannInt_P15 [lemma, in RiemannInt_P15]
RiemannInt_P9 [lemma, in RiemannInt_P9]
RiemannInt_P3 [lemma, in RiemannInt_P3]
RiemannInt_P28 [lemma, in RiemannInt_P28]
RiemannInt_P12 [lemma, in RiemannInt_P12]
RiemannInt_P17 [lemma, in RiemannInt_P17]
RiemannInt_P23 [lemma, in RiemannInt_P23]
RiemannInt_P13 [lemma, in RiemannInt_P13]
RiemannInt_P19 [lemma, in RiemannInt_P19]
RiemannInt_P4 [lemma, in RiemannInt_P4]
RiemannInt_P32 [lemma, in RiemannInt_P32]
RiemannInt_P30 [lemma, in RiemannInt_P30]
RiemannInt_SF [definition, in RiemannInt_SF]
RiemannInt_P1 [lemma, in RiemannInt_P1]
RiemannInt_P8 [lemma, in RiemannInt_P8]
RiemannInt_P7 [lemma, in RiemannInt_P7]
RiemannInt_P29 [lemma, in RiemannInt_P29]
RiemannInt_P10 [lemma, in RiemannInt_P10]
RiemannInt_P26 [lemma, in RiemannInt_P26]
RiemannInt_P18 [lemma, in RiemannInt_P18]
RiemannInt_P14 [lemma, in RiemannInt_P14]
RiemannInt_P24 [lemma, in RiemannInt_P24]
RiemannInt_P21 [lemma, in RiemannInt_P21]
RiemannInt_P2 [lemma, in RiemannInt_P2]
RiemannInt_P11 [lemma, in RiemannInt_P11]
RiemannInt_P5 [lemma, in RiemannInt_P5]
RiemannInt_exists [lemma, in RiemannInt_exists]
RiemannInt_P27 [lemma, in RiemannInt_P27]
RiemannInt_P22 [lemma, in RiemannInt_P22]
RiemannInt_SF [library]
Riemann_integrable [definition, in Riemann_integrable]
right [constructor, in right]
RightDistributivityImplicationOverDisjunction [definition, in RightDistributivityImplicationOverDisjunction]
right_prefix [lemma, in right_prefix]
right_sym [constructor, in right_sym]
right_lex [constructor, in right_lex]
RIneq [library]
ring_theory_switch_eq [lemma, in ring_theory_switch_eq]
Ring31 [library]
Rinv [axiom, in Rinv]
RinvN [definition, in RinvN]
RinvN_cv [lemma, in RinvN_cv]
RinvN_pos [lemma, in RinvN_pos]
Rinv_1 [lemma, in Rinv_1]
Rinv_lt_0_compat [lemma, in Rinv_lt_0_compat]
Rinv_mult_distr [lemma, in Rinv_mult_distr]
Rinv_mult_simpl [lemma, in Rinv_mult_simpl]
Rinv_r_sym [lemma, in Rinv_r_sym]
Rinv_l [axiom, in Rinv_l]
Rinv_r [lemma, in Rinv_r]
Rinv_pow [lemma, in Rinv_pow]
Rinv_neq_0_compat [lemma, in Rinv_neq_0_compat]
Rinv_r_simpl_m [lemma, in Rinv_r_simpl_m]
Rinv_r_simpl_l [lemma, in Rinv_r_simpl_l]
Rinv_1_lt_contravar [lemma, in Rinv_1_lt_contravar]
Rinv_0_lt_compat [lemma, in Rinv_0_lt_compat]
Rinv_Rdiv [lemma, in Rinv_Rdiv]
Rinv_l_sym [lemma, in Rinv_l_sym]
Rinv_r_simpl_r [lemma, in Rinv_r_simpl_r]
Rinv_involutive [lemma, in Rinv_involutive]
Rinv_lt_contravar [lemma, in Rinv_lt_contravar]
Rle [definition, in Rle]
RLegacyTheory [lemma, in RLegacyTheory]
Rlength [definition, in Rlength]
Rle_dec [lemma, in Rle_dec]
Rle_max_compat_l [lemma, in Rle_max_compat_l]
Rle_trans [lemma, in Rle_trans]
Rle_not_lt [lemma, in Rle_not_lt]
Rle_Qle [lemma, in Rle_Qle]
Rle_min_compat_l [lemma, in Rle_min_compat_l]
Rle_ge [lemma, in Rle_ge]
Rle_cv_lim [lemma, in Rle_cv_lim]
Rle_antisym [lemma, in Rle_antisym]
Rle_Rinv [lemma, in Rle_Rinv]
Rle_0_1 [lemma, in Rle_0_1]
Rle_abs [lemma, in Rle_abs]
Rle_0_sqr [lemma, in Rle_0_sqr]
Rle_Rpower [lemma, in Rle_Rpower]
Rle_max_compat_r [lemma, in Rle_max_compat_r]
Rle_not_gt [lemma, in Rle_not_gt]
Rle_or_lt [lemma, in Rle_or_lt]
Rle_minus [lemma, in Rle_minus]
Rle_lt_or_eq_dec [lemma, in Rle_lt_or_eq_dec]
Rle_refl [lemma, in Rle_refl]
Rle_lt_dec [lemma, in Rle_lt_dec]
Rle_le_eq [lemma, in Rle_le_eq]
Rle_lt_trans [lemma, in Rle_lt_trans]
Rle_lt_0_plus_1 [lemma, in Rle_lt_0_plus_1]
Rle_pow [lemma, in Rle_pow]
Rle_min_compat_r [lemma, in Rle_min_compat_r]
Rlimit [library]
Rlist [inductive, in Rlist]
RList [library]
RList_P6 [lemma, in RList_P6]
RList_P18 [lemma, in RList_P18]
RList_P25 [lemma, in RList_P25]
RList_P29 [lemma, in RList_P29]
RList_P17 [lemma, in RList_P17]
RList_P16 [lemma, in RList_P16]
RList_P20 [lemma, in RList_P20]
RList_P12 [lemma, in RList_P12]
RList_P19 [lemma, in RList_P19]
RList_P10 [lemma, in RList_P10]
RList_P21 [lemma, in RList_P21]
RList_P0 [lemma, in RList_P0]
RList_P7 [lemma, in RList_P7]
RList_P8 [lemma, in RList_P8]
RList_P9 [lemma, in RList_P9]
RList_P5 [lemma, in RList_P5]
RList_P1 [lemma, in RList_P1]
RList_P14 [lemma, in RList_P14]
Rlist_P1 [lemma, in Rlist_P1]
RList_P28 [lemma, in RList_P28]
RList_P15 [lemma, in RList_P15]
RList_P2 [lemma, in RList_P2]
RList_P26 [lemma, in RList_P26]
RList_P27 [lemma, in RList_P27]
RList_P24 [lemma, in RList_P24]
RList_P3 [lemma, in RList_P3]
RList_P4 [lemma, in RList_P4]
RList_P13 [lemma, in RList_P13]
RList_P11 [lemma, in RList_P11]
RList_P23 [lemma, in RList_P23]
RList_P22 [lemma, in RList_P22]
Rln [definition, in Rln]
Rlogic [library]
Rlt [axiom, in Rlt]
Rlt_gt [lemma, in Rlt_gt]
Rlt_plus_1 [lemma, in Rlt_plus_1]
Rlt_not_le [lemma, in Rlt_not_le]
Rlt_asym [axiom, in Rlt_asym]
Rlt_dec [lemma, in Rlt_dec]
Rlt_PI_3PI2 [lemma, in Rlt_PI_3PI2]
Rlt_eps2_eps [lemma, in Rlt_eps2_eps]
Rlt_R0_R2 [lemma, in Rlt_R0_R2]
Rlt_0_1 [lemma, in Rlt_0_1]
Rlt_Rminus [lemma, in Rlt_Rminus]
Rlt_or_le [lemma, in Rlt_or_le]
Rlt_eps4_eps [lemma, in Rlt_eps4_eps]
Rlt_eq_compat [lemma, in Rlt_eq_compat]
Rlt_le_dec [lemma, in Rlt_le_dec]
Rlt_pow [lemma, in Rlt_pow]
Rlt_Qlt [lemma, in Rlt_Qlt]
Rlt_irrefl [lemma, in Rlt_irrefl]
Rlt_minus [lemma, in Rlt_minus]
Rlt_le_trans [lemma, in Rlt_le_trans]
Rlt_sqrt2_0 [lemma, in Rlt_sqrt2_0]
Rlt_4 [lemma, in Rlt_4]
Rlt_pow_R1 [lemma, in Rlt_pow_R1]
Rlt_0_sqr [lemma, in Rlt_0_sqr]
Rlt_trans [axiom, in Rlt_trans]
Rlt_le [lemma, in Rlt_le]
Rlt_not_ge [lemma, in Rlt_not_ge]
Rlt_not_eq [lemma, in Rlt_not_eq]
Rlt_dichotomy_converse [lemma, in Rlt_dichotomy_converse]
Rlt_3PI2_2PI [lemma, in Rlt_3PI2_2PI]
Rlt_sqrt3_0 [lemma, in Rlt_sqrt3_0]
Rmax [definition, in Rmax]
RmaxAbs [lemma, in RmaxAbs]
RmaxLess1 [abbreviation, in RmaxLess1]
RmaxLess2 [abbreviation, in RmaxLess2]
RmaxRmult [lemma, in RmaxRmult]
RmaxSym [abbreviation, in RmaxSym]
Rmax_right [lemma, in Rmax_right]
Rmax_comm [lemma, in Rmax_comm]
Rmax_r [lemma, in Rmax_r]
Rmax_r [lemma, in Rmax_r]
Rmax_lub [lemma, in Rmax_lub]
Rmax_Rle [lemma, in Rmax_Rle]
Rmax_case [lemma, in Rmax_case]
Rmax_case_strong [lemma, in Rmax_case_strong]
Rmax_stable_in_negreal [lemma, in Rmax_stable_in_negreal]
Rmax_l [lemma, in Rmax_l]
Rmax_l [lemma, in Rmax_l]
Rmax_lub_lt [lemma, in Rmax_lub_lt]
Rmax_neg [lemma, in Rmax_neg]
Rmax_left [lemma, in Rmax_left]
Rmax_N [definition, in Rmax_N]
Rmin [definition, in Rmin]
Rminmax [library]
Rminus [definition, in Rminus]
Rminus_Int_part2 [lemma, in Rminus_Int_part2]
Rminus_Int_part1 [lemma, in Rminus_Int_part1]
Rminus_not_eq_right [lemma, in Rminus_not_eq_right]
Rminus_not_eq [lemma, in Rminus_not_eq]
Rminus_gt [lemma, in Rminus_gt]
Rminus_lt [lemma, in Rminus_lt]
Rminus_eq_contra [lemma, in Rminus_eq_contra]
Rminus_ge [lemma, in Rminus_ge]
Rminus_diag_uniq_sym [lemma, in Rminus_diag_uniq_sym]
Rminus_diag_eq [lemma, in Rminus_diag_eq]
Rminus_fp2 [lemma, in Rminus_fp2]
Rminus_fp1 [lemma, in Rminus_fp1]
Rminus_diag_uniq [lemma, in Rminus_diag_uniq]
Rminus_0_r [lemma, in Rminus_0_r]
Rminus_le [lemma, in Rminus_le]
Rminus_0_l [lemma, in Rminus_0_l]
Rmin_pos [lemma, in Rmin_pos]
Rmin_pos [abbreviation, in Rmin_pos]
Rmin_glb [lemma, in Rmin_glb]
Rmin_left [lemma, in Rmin_left]
Rmin_case_strong [lemma, in Rmin_case_strong]
Rmin_Rgt [lemma, in Rmin_Rgt]
Rmin_r [lemma, in Rmin_r]
Rmin_r [lemma, in Rmin_r]
Rmin_2 [abbreviation, in Rmin_2]
Rmin_l [lemma, in Rmin_l]
Rmin_l [lemma, in Rmin_l]
Rmin_stable_in_posreal [lemma, in Rmin_stable_in_posreal]
Rmin_case [lemma, in Rmin_case]
Rmin_Rgt_r [lemma, in Rmin_Rgt_r]
Rmin_right [lemma, in Rmin_right]
Rmin_Rgt_l [lemma, in Rmin_Rgt_l]
Rmin_comm [lemma, in Rmin_comm]
Rmin_glb_lt [lemma, in Rmin_glb_lt]
Rmult [axiom, in Rmult]
Rmult_plus_distr_l [axiom, in Rmult_plus_distr_l]
Rmult_gt_0_lt_compat [lemma, in Rmult_gt_0_lt_compat]
Rmult_gt_reg_l [lemma, in Rmult_gt_reg_l]
Rmult_minus_distr_l [lemma, in Rmult_minus_distr_l]
Rmult_gt_0_compat [lemma, in Rmult_gt_0_compat]
Rmult_le_compat_l [lemma, in Rmult_le_compat_l]
Rmult_assoc [axiom, in Rmult_assoc]
Rmult_eq_0_compat_r [lemma, in Rmult_eq_0_compat_r]
Rmult_le_0_lt_compat [lemma, in Rmult_le_0_lt_compat]
Rmult_eq_0_compat [lemma, in Rmult_eq_0_compat]
Rmult_eq_reg_l [lemma, in Rmult_eq_reg_l]
Rmult_integral [lemma, in Rmult_integral]
Rmult_opp_opp [lemma, in Rmult_opp_opp]
Rmult_eq_reg_r [lemma, in Rmult_eq_reg_r]
Rmult_1_r [lemma, in Rmult_1_r]
Rmult_neq_0_reg [lemma, in Rmult_neq_0_reg]
Rmult_le_reg_l [lemma, in Rmult_le_reg_l]
Rmult_integral_contrapositive_currified [lemma, in Rmult_integral_contrapositive_currified]
Rmult_lt_0_compat [lemma, in Rmult_lt_0_compat]
Rmult_ge_compat_r [lemma, in Rmult_ge_compat_r]
Rmult_le_pos [lemma, in Rmult_le_pos]
Rmult_le_compat [lemma, in Rmult_le_compat]
Rmult_le_ge_compat_neg_l [lemma, in Rmult_le_ge_compat_neg_l]
Rmult_eq_compat_r [lemma, in Rmult_eq_compat_r]
Rmult_lt_gt_compat_neg_l [lemma, in Rmult_lt_gt_compat_neg_l]
Rmult_1_l [axiom, in Rmult_1_l]
Rmult_0_l [lemma, in Rmult_0_l]
Rmult_ge_compat_l [lemma, in Rmult_ge_compat_l]
Rmult_plus_distr_r [lemma, in Rmult_plus_distr_r]
Rmult_ne [lemma, in Rmult_ne]
Rmult_integral_contrapositive [lemma, in Rmult_integral_contrapositive]
Rmult_ge_0_gt_0_lt_compat [lemma, in Rmult_ge_0_gt_0_lt_compat]
Rmult_le_compat_r [lemma, in Rmult_le_compat_r]
Rmult_0_r [lemma, in Rmult_0_r]
Rmult_ge_compat [lemma, in Rmult_ge_compat]
Rmult_le_reg_r [lemma, in Rmult_le_reg_r]
Rmult_eq_compat_l [lemma, in Rmult_eq_compat_l]
Rmult_lt_compat_r [lemma, in Rmult_lt_compat_r]
Rmult_comm [axiom, in Rmult_comm]
Rmult_gt_compat_l [lemma, in Rmult_gt_compat_l]
Rmult_le_compat_neg_l [lemma, in Rmult_le_compat_neg_l]
Rmult_lt_compat_l [axiom, in Rmult_lt_compat_l]
Rmult_eq_0_compat_l [lemma, in Rmult_eq_0_compat_l]
Rmult_lt_reg_l [lemma, in Rmult_lt_reg_l]
Rmult_lt_reg_r [lemma, in Rmult_lt_reg_r]
Rmult_gt_compat_r [lemma, in Rmult_gt_compat_r]
Rnot_ge_lt [lemma, in Rnot_ge_lt]
Rnot_gt_ge [lemma, in Rnot_gt_ge]
Rnot_le_gt [lemma, in Rnot_le_gt]
Rnot_lt_ge [lemma, in Rnot_lt_ge]
Rnot_lt_le [lemma, in Rnot_lt_le]
Rnot_le_lt [lemma, in Rnot_le_lt]
Rnot_gt_le [lemma, in Rnot_gt_le]
Rnot_ge_gt [lemma, in Rnot_ge_gt]
Rolle [lemma, in Rolle]
Ropp [axiom, in Ropp]
Ropp_lt_gt_contravar [lemma, in Ropp_lt_gt_contravar]
Ropp_involutive [lemma, in Ropp_involutive]
Ropp_0_ge_le_contravar [lemma, in Ropp_0_ge_le_contravar]
Ropp_plus_distr [lemma, in Ropp_plus_distr]
Ropp_le_cancel [lemma, in Ropp_le_cancel]
Ropp_gt_contravar [lemma, in Ropp_gt_contravar]
Ropp_div [lemma, in Ropp_div]
Ropp_minus_distr [lemma, in Ropp_minus_distr]
Ropp_ge_cancel [lemma, in Ropp_ge_cancel]
Ropp_gt_cancel [lemma, in Ropp_gt_cancel]
Ropp_lt_contravar [lemma, in Ropp_lt_contravar]
Ropp_gt_lt_contravar [lemma, in Ropp_gt_lt_contravar]
Ropp_ge_le_contravar [lemma, in Ropp_ge_le_contravar]
Ropp_mult_distr_l_reverse [lemma, in Ropp_mult_distr_l_reverse]
Ropp_Ropp_IZR [definition, in Ropp_Ropp_IZR]
Ropp_lt_gt_0_contravar [lemma, in Ropp_lt_gt_0_contravar]
Ropp_le_ge_contravar [lemma, in Ropp_le_ge_contravar]
Ropp_neq_0_compat [lemma, in Ropp_neq_0_compat]
Ropp_gt_lt_0_contravar [lemma, in Ropp_gt_lt_0_contravar]
Ropp_le_contravar [lemma, in Ropp_le_contravar]
Ropp_mult_distr_r_reverse [lemma, in Ropp_mult_distr_r_reverse]
Ropp_0_gt_lt_contravar [lemma, in Ropp_0_gt_lt_contravar]
Ropp_0 [lemma, in Ropp_0]
Ropp_eq_0_compat [lemma, in Ropp_eq_0_compat]
Ropp_eq_compat [lemma, in Ropp_eq_compat]
Ropp_lt_cancel [lemma, in Ropp_lt_cancel]
Ropp_inv_permute [lemma, in Ropp_inv_permute]
Ropp_minus_distr' [lemma, in Ropp_minus_distr']
Ropp_0_lt_gt_contravar [lemma, in Ropp_0_lt_gt_contravar]
Ropp_0_le_ge_contravar [lemma, in Ropp_0_le_ge_contravar]
Ropp_ge_contravar [lemma, in Ropp_ge_contravar]
ROrder [module, in ROrder]
ROrderedType [library]
rotation_0 [lemma, in rotation_0]
rotation_PI2 [lemma, in rotation_PI2]
Rplus [axiom, in Rplus]
Rplus [inductive, in Rplus]
Rplus_ge_compat [lemma, in Rplus_ge_compat]
Rplus_n [constructor, in Rplus_n]
Rplus_0_l [axiom, in Rplus_0_l]
Rplus_lt_reg_pos_r [lemma, in Rplus_lt_reg_pos_r]
Rplus_gt_reg_neg_r [lemma, in Rplus_gt_reg_neg_r]
Rplus_assoc [axiom, in Rplus_assoc]
Rplus_sqr_eq_0 [lemma, in Rplus_sqr_eq_0]
Rplus_le_compat_r [lemma, in Rplus_le_compat_r]
Rplus_le_reg_l [lemma, in Rplus_le_reg_l]
Rplus_opp_r [axiom, in Rplus_opp_r]
Rplus_gt_compat_r [lemma, in Rplus_gt_compat_r]
Rplus_lt_le_compat [lemma, in Rplus_lt_le_compat]
Rplus_le_compat_l [lemma, in Rplus_le_compat_l]
Rplus_0 [constructor, in Rplus_0]
Rplus_opp_l [lemma, in Rplus_opp_l]
Rplus_0_r_uniq [lemma, in Rplus_0_r_uniq]
Rplus_gt_compat_l [lemma, in Rplus_gt_compat_l]
Rplus_le_compat [lemma, in Rplus_le_compat]
Rplus_ge_compat_r [lemma, in Rplus_ge_compat_r]
Rplus_minus [lemma, in Rplus_minus]
Rplus_0_r [lemma, in Rplus_0_r]
Rplus_le_reg_pos_r [lemma, in Rplus_le_reg_pos_r]
Rplus_eq_R0 [lemma, in Rplus_eq_R0]
Rplus_lt_compat_l [axiom, in Rplus_lt_compat_l]
Rplus_sqr_eq_0_l [lemma, in Rplus_sqr_eq_0_l]
Rplus_ge_reg_l [lemma, in Rplus_ge_reg_l]
Rplus_lt_0_compat [lemma, in Rplus_lt_0_compat]
Rplus_gt_reg_l [lemma, in Rplus_gt_reg_l]
Rplus_ge_gt_compat [lemma, in Rplus_ge_gt_compat]
Rplus_gt_ge_compat [lemma, in Rplus_gt_ge_compat]
Rplus_contains_R [lemma, in Rplus_contains_R]
Rplus_eq_0_l [lemma, in Rplus_eq_0_l]
Rplus_lt_reg_r [lemma, in Rplus_lt_reg_r]
Rplus_ge_compat_l [lemma, in Rplus_ge_compat_l]
Rplus_opp_r_uniq [lemma, in Rplus_opp_r_uniq]
Rplus_ge_reg_neg_r [lemma, in Rplus_ge_reg_neg_r]
Rplus_comm [axiom, in Rplus_comm]
Rplus_lt_pos [abbreviation, in Rplus_lt_pos]
Rplus_ne [lemma, in Rplus_ne]
Rplus_lt_compat [lemma, in Rplus_lt_compat]
Rplus_le_lt_0_compat [lemma, in Rplus_le_lt_0_compat]
Rplus_le_lt_compat [lemma, in Rplus_le_lt_compat]
Rplus_eq_compat_l [lemma, in Rplus_eq_compat_l]
Rplus_eq_reg_l [lemma, in Rplus_eq_reg_l]
Rplus_lt_le_0_compat [lemma, in Rplus_lt_le_0_compat]
Rplus_le_reg_r [lemma, in Rplus_le_reg_r]
Rplus_le_le_0_compat [lemma, in Rplus_le_le_0_compat]
Rplus_gt_compat [lemma, in Rplus_gt_compat]
Rplus_lt_compat_r [lemma, in Rplus_lt_compat_r]
Rpower [definition, in Rpower]
Rpower [library]
Rpower_mult [lemma, in Rpower_mult]
Rpower_O [lemma, in Rpower_O]
Rpower_plus [lemma, in Rpower_plus]
Rpower_1 [lemma, in Rpower_1]
Rpower_Ropp [lemma, in Rpower_Ropp]
Rpower_pow [lemma, in Rpower_pow]
Rpower_sqrt [lemma, in Rpower_sqrt]
Rpower_lt [lemma, in Rpower_lt]
RPow_abs [lemma, in RPow_abs]
Rpow_mult_distr [lemma, in Rpow_mult_distr]
Rpow_def [library]
Rprod [library]
RRle_abs [definition, in RRle_abs]
Rsepare [lemma, in Rsepare]
Rseries [library]
Rseries_CV_comp [lemma, in Rseries_CV_comp]
Rsigma [library]
Rsqr [definition, in Rsqr]
Rsqrt [definition, in Rsqrt]
Rsqrt_Rsqrt [lemma, in Rsqrt_Rsqrt]
Rsqrt_exists [lemma, in Rsqrt_exists]
Rsqrt_positivity [lemma, in Rsqrt_positivity]
Rsqrt_def [library]
Rsqr_plus_minus [lemma, in Rsqr_plus_minus]
Rsqr_mult [lemma, in Rsqr_mult]
Rsqr_abs [lemma, in Rsqr_abs]
Rsqr_0 [lemma, in Rsqr_0]
Rsqr_incr_1 [lemma, in Rsqr_incr_1]
Rsqr_eq_0 [lemma, in Rsqr_eq_0]
Rsqr_0_uniq [lemma, in Rsqr_0_uniq]
Rsqr_plus [lemma, in Rsqr_plus]
Rsqr_minus_plus [lemma, in Rsqr_minus_plus]
Rsqr_gt_0_0 [lemma, in Rsqr_gt_0_0]
Rsqr_1 [lemma, in Rsqr_1]
Rsqr_eq_abs_0 [lemma, in Rsqr_eq_abs_0]
Rsqr_eq [lemma, in Rsqr_eq]
Rsqr_incrst_1 [lemma, in Rsqr_incrst_1]
Rsqr_neg_minus [lemma, in Rsqr_neg_minus]
Rsqr_neg_pos_le_1 [lemma, in Rsqr_neg_pos_le_1]
Rsqr_incr_0_var [lemma, in Rsqr_incr_0_var]
Rsqr_lt_abs_0 [lemma, in Rsqr_lt_abs_0]
Rsqr_inv [lemma, in Rsqr_inv]
Rsqr_le_abs_0 [lemma, in Rsqr_le_abs_0]
Rsqr_neg [lemma, in Rsqr_neg]
Rsqr_incr_0 [lemma, in Rsqr_incr_0]
Rsqr_eq_asb_1 [lemma, in Rsqr_eq_asb_1]
Rsqr_minus [lemma, in Rsqr_minus]
Rsqr_sqrt [lemma, in Rsqr_sqrt]
Rsqr_sin_cos_d_one [lemma, in Rsqr_sin_cos_d_one]
Rsqr_le_abs_1 [lemma, in Rsqr_le_abs_1]
Rsqr_incrst_0 [lemma, in Rsqr_incrst_0]
Rsqr_sol_eq_0_1 [lemma, in Rsqr_sol_eq_0_1]
Rsqr_div [lemma, in Rsqr_div]
Rsqr_sol_eq_0_0 [lemma, in Rsqr_sol_eq_0_0]
Rsqr_lt_abs_1 [lemma, in Rsqr_lt_abs_1]
Rsqr_inj [lemma, in Rsqr_inj]
Rsqr_neg_pos_le_0 [lemma, in Rsqr_neg_pos_le_0]
Rsqr_pos_lt [lemma, in Rsqr_pos_lt]
Rstar [inductive, in Rstar]
RstarRplus_RRstar [lemma, in RstarRplus_RRstar]
Rstar_transitive [lemma, in Rstar_transitive]
Rstar_0 [constructor, in Rstar_0]
Rstar_reflexive [lemma, in Rstar_reflexive]
Rstar_cases [lemma, in Rstar_cases]
Rstar_equiv_Rstar1 [lemma, in Rstar_equiv_Rstar1]
Rstar_contains_Rplus [lemma, in Rstar_contains_Rplus]
Rstar_imp_coherent [lemma, in Rstar_imp_coherent]
Rstar_contains_R [lemma, in Rstar_contains_R]
Rstar_n [constructor, in Rstar_n]
Rstar1 [inductive, in Rstar1]
Rstar1_n [constructor, in Rstar1_n]
Rstar1_1 [constructor, in Rstar1_1]
Rstar1_0 [constructor, in Rstar1_0]
rstn1_refl [constructor, in rstn1_refl]
rstn1_trans [constructor, in rstn1_trans]
rst_refl [constructor, in rst_refl]
rst_trans [constructor, in rst_trans]
rst_step [constructor, in rst_step]
rst_sym [constructor, in rst_sym]
rst1n_trans [constructor, in rst1n_trans]
rst1n_refl [constructor, in rst1n_refl]
Rsum_abs [lemma, in Rsum_abs]
Rsym_imp_Rstarsym [lemma, in Rsym_imp_Rstarsym]
Rsym_imp_notRsym [lemma, in Rsym_imp_notRsym]
Rtail [definition, in Rtail]
rtn1_trans_equiv [abbreviation, in rtn1_trans_equiv]
rtn1_refl [constructor, in rtn1_refl]
rtn1_trans [constructor, in rtn1_trans]
rtn1_trans [abbreviation, in rtn1_trans]
Rtopology [library]
Rtotal_order [lemma, in Rtotal_order]
Rtrigo [library]
Rtrigo_alt [library]
Rtrigo_def [library]
Rtrigo_fun [library]
Rtrigo_calc [library]
Rtrigo_reg [library]
Rtrigo1 [library]
rtsn1_rts [abbreviation, in rtsn1_rts]
rtsn1_refl [abbreviation, in rtsn1_refl]
rtsn1_sym [abbreviation, in rtsn1_sym]
rtsn1_trans [abbreviation, in rtsn1_trans]
rtsn1_trans [abbreviation, in rtsn1_trans]
rts_rts1n [abbreviation, in rts_rts1n]
rts_rtsn1 [abbreviation, in rts_rtsn1]
rts_rts1n_equiv [abbreviation, in rts_rts1n_equiv]
rts_rtsn1_equiv [abbreviation, in rts_rtsn1_equiv]
rts_1n_trans [abbreviation, in rts_1n_trans]
rts1n_refl [abbreviation, in rts1n_refl]
rts1n_sym [abbreviation, in rts1n_sym]
rts1n_rts [abbreviation, in rts1n_rts]
rts1n_trans [abbreviation, in rts1n_trans]
rt_step [constructor, in rt_step]
rt_refl [constructor, in rt_refl]
rt_trans [constructor, in rt_trans]
rt1n_refl [constructor, in rt1n_refl]
rt1n_trans_equiv [abbreviation, in rt1n_trans_equiv]
rt1n_trans [constructor, in rt1n_trans]
rt1n_trans [abbreviation, in rt1n_trans]
rt1n_ind_right [lemma, in rt1n_ind_right]
R_as_UBE.eqb [definition, in eqb]
R_as_OT.le_lteq [lemma, in le_lteq]
R_as_OT [module, in R_as_OT]
R_as_OT.lt_compat [instance, in lt_compat]
R_as_OT.lt_strorder [instance, in lt_strorder]
R_rt1n [abbreviation, in R_rt1n]
R_dist_eq [lemma, in R_dist_eq]
R_dist [definition, in R_dist]
R_dist_sym [lemma, in R_dist_sym]
R_as_UBE.t [definition, in t]
R_as_OT.le [definition, in le]
R_as_OT.compare_spec [definition, in compare_spec]
R_complete [lemma, in R_complete]
R_met [definition, in R_met]
R_as_DT [module, in R_as_DT]
R_sanity [lemma, in R_sanity]
R_as_OT.compare [definition, in compare]
R_dist_plus [lemma, in R_dist_plus]
R_rtn1 [abbreviation, in R_rtn1]
R_as_UBE.eqb_eq [definition, in eqb_eq]
R_dist_refl [lemma, in R_dist_refl]
R_dist_pos [lemma, in R_dist_pos]
R_as_UBE [module, in R_as_UBE]
R_dist_tri [lemma, in R_dist_tri]
R_as_OT.lt [definition, in lt]
R_as_UBE.eq [definition, in eq]
R_sqrt [library]
R_Ifp [library]
R_sqr [library]
R.minus_min_distr_r [lemma, in minus_min_distr_r]
R.minus_min_distr_l [lemma, in minus_min_distr_l]
R.minus_max_distr_l [lemma, in minus_max_distr_l]
R.minus_max_distr_r [lemma, in minus_max_distr_r]
R.opp_min_distr [lemma, in opp_min_distr]
R.opp_max_distr [lemma, in opp_max_distr]
R.plus_max_distr_l [lemma, in plus_max_distr_l]
R.plus_max_distr_r [lemma, in plus_max_distr_r]
R.plus_min_distr_l [lemma, in plus_min_distr_l]
R.plus_min_distr_r [lemma, in plus_min_distr_r]
R0 [axiom, in R0]
R0_fp_O [lemma, in R0_fp_O]
R1 [axiom, in R1]
R1_sqrt2_neq_0 [lemma, in R1_sqrt2_neq_0]
R1_neq_R0 [axiom, in R1_neq_R0]



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)