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 _ (13564 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 _ (95 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 _ (211 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 _ (71 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 _ (6947 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 _ (305 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 _ (352 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 _ (295 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 _ (183 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 _ (2870 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 _ (287 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 _ (433 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 _ (1189 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 _ (326 entries)

R

R [axiom, in Coq.Reals.Rdefinitions]
R [definition, in Coq.Logic.Berardi]
R [definition, in Coq.Logic.ConstructiveEpsilon]
R [definition, in Coq.ZArith.Wf_Z]
R [module, in Coq.FSets.FMapAVL]
R [definition, in Coq.Sets.Cpo]
Rabs [definition, in Coq.Reals.Rbasic_fun]
Rabs_def1 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_def2 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_derive_1 [lemma, in Coq.Reals.Ranalysis4]
Rabs_derive_2 [lemma, in Coq.Reals.Ranalysis4]
Rabs_left [lemma, in Coq.Reals.Rbasic_fun]
Rabs_left1 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_minus_sym [lemma, in Coq.Reals.Rbasic_fun]
Rabs_mult [lemma, in Coq.Reals.Rbasic_fun]
Rabs_no_R0 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_pos [lemma, in Coq.Reals.Rbasic_fun]
Rabs_pos_eq [lemma, in Coq.Reals.Rbasic_fun]
Rabs_pos_lt [lemma, in Coq.Reals.Rbasic_fun]
Rabs_Rabsolu [lemma, in Coq.Reals.Rbasic_fun]
Rabs_right [lemma, in Coq.Reals.Rbasic_fun]
Rabs_Rinv [lemma, in Coq.Reals.Rbasic_fun]
Rabs_Ropp [lemma, in Coq.Reals.Rbasic_fun]
Rabs_R0 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_R1 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_triang [lemma, in Coq.Reals.Rbasic_fun]
Rabs_triang_gen [lemma, in Coq.Reals.PartSum]
Rabs_triang_inv [lemma, in Coq.Reals.Rbasic_fun]
Rabs_triang_inv2 [lemma, in Coq.Reals.Rbasic_fun]
Rabs_Zabs [lemma, in Coq.Reals.Rbasic_fun]
Rabs_4 [lemma, in Coq.Reals.Ranalysis2]
rad_deg [lemma, in Coq.Reals.Rtrigo_calc]
Ranalysis [library]
Ranalysis1 [library]
Ranalysis2 [library]
Ranalysis3 [library]
Ranalysis4 [library]
Raw [module, in Coq.FSets.FSetWeakList]
Raw [module, in Coq.FSets.FSetList]
Raw [module, in Coq.FSets.FMapFullAVL]
Raw [module, in Coq.FSets.FMapList]
Raw [module, in Coq.FSets.FMapAVL]
Raw [module, in Coq.FSets.FMapList]
Raw [module, in Coq.FSets.FSetWeakList]
Raw [module, in Coq.FSets.FSetFullAVL]
Raw [module, in Coq.FSets.FSetList]
Raw [module, in Coq.FSets.FSetAVL]
Raw [module, in Coq.FSets.FMapWeakList]
Raw [module, in Coq.FSets.FMapAVL]
Raw [module, in Coq.FSets.FMapWeakList]
Raw [module, in Coq.FSets.FSetAVL]
Raw.add [definition, in Coq.FSets.FSetWeakList]
Raw.add [definition, in Coq.FSets.FSetAVL]
Raw.add [definition, in Coq.FSets.FMapAVL]
Raw.add [definition, in Coq.FSets.FSetList]
Raw.add_eq [lemma, in Coq.FSets.FMapWeakList]
Raw.add_Inf [lemma, in Coq.FSets.FSetList]
Raw.add_Inf [lemma, in Coq.FSets.FMapList]
Raw.add_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.add_not_eq [lemma, in Coq.FSets.FMapWeakList]
Raw.add_sort [lemma, in Coq.FSets.FSetList]
Raw.add_sorted [lemma, in Coq.FSets.FMapList]
Raw.add_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.add_1 [lemma, in Coq.FSets.FMapList]
Raw.add_1 [lemma, in Coq.FSets.FSetList]
Raw.add_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.add_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.add_2 [lemma, in Coq.FSets.FMapList]
Raw.add_2 [lemma, in Coq.FSets.FSetList]
Raw.add_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.add_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.add_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.add_3 [lemma, in Coq.FSets.FMapList]
Raw.add_3 [lemma, in Coq.FSets.FMapWeakList]
Raw.add_3 [lemma, in Coq.FSets.FSetList]
Raw.add_3' [lemma, in Coq.FSets.FMapWeakList]
Raw.assert_false [definition, in Coq.FSets.FSetAVL]
Raw.assert_false [definition, in Coq.FSets.FMapAVL]
Raw.at_least_left [definition, in Coq.FSets.FMapWeakList]
Raw.at_least_one [definition, in Coq.FSets.FMapWeakList]
Raw.at_least_one [definition, in Coq.FSets.FMapList]
Raw.at_least_one_then_f [definition, in Coq.FSets.FMapList]
Raw.at_least_one_then_f [definition, in Coq.FSets.FMapWeakList]
Raw.at_least_right [definition, in Coq.FSets.FMapWeakList]
Raw.bal [definition, in Coq.FSets.FMapAVL]
Raw.bal [definition, in Coq.FSets.FSetAVL]
Raw.BSLeaf [constructor, in Coq.FSets.FSetAVL]
Raw.BSLeaf [constructor, in Coq.FSets.FMapAVL]
Raw.BSNode [constructor, in Coq.FSets.FSetAVL]
Raw.BSNode [constructor, in Coq.FSets.FMapAVL]
Raw.bst [inductive, in Coq.FSets.FSetAVL]
Raw.bst [inductive, in Coq.FSets.FMapAVL]
Raw.cardinal [definition, in Coq.FSets.FMapAVL]
Raw.cardinal [definition, in Coq.FSets.FSetList]
Raw.cardinal [definition, in Coq.FSets.FSetAVL]
Raw.cardinal [definition, in Coq.FSets.FSetWeakList]
Raw.cardinal_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.cardinal_1 [lemma, in Coq.FSets.FSetList]
Raw.check [definition, in Coq.FSets.FMapWeakList]
Raw.choose [definition, in Coq.FSets.FSetWeakList]
Raw.choose [definition, in Coq.FSets.FSetList]
Raw.choose [definition, in Coq.FSets.FSetAVL]
Raw.choose_1 [definition, in Coq.FSets.FSetWeakList]
Raw.choose_1 [definition, in Coq.FSets.FSetList]
Raw.choose_2 [definition, in Coq.FSets.FSetWeakList]
Raw.choose_2 [definition, in Coq.FSets.FSetList]
Raw.choose_3 [lemma, in Coq.FSets.FSetList]
Raw.combine [definition, in Coq.FSets.FMapWeakList]
Raw.combine [definition, in Coq.FSets.FMapList]
Raw.combine_l [definition, in Coq.FSets.FMapWeakList]
Raw.combine_lelistA [lemma, in Coq.FSets.FMapList]
Raw.combine_l_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.combine_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.combine_r [definition, in Coq.FSets.FMapWeakList]
Raw.combine_r_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.combine_sorted [lemma, in Coq.FSets.FMapList]
Raw.combine_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.combine_1 [lemma, in Coq.FSets.FMapList]
Raw.compare [definition, in Coq.FSets.FSetAVL]
Raw.compare [definition, in Coq.FSets.FSetList]
Raw.compare_cont [definition, in Coq.FSets.FSetAVL]
Raw.compare_end [definition, in Coq.FSets.FSetAVL]
Raw.compare_more [definition, in Coq.FSets.FSetAVL]
Raw.concat [definition, in Coq.FSets.FMapAVL]
Raw.concat [definition, in Coq.FSets.FSetAVL]
Raw.cons [definition, in Coq.FSets.FMapAVL]
Raw.cons [definition, in Coq.FSets.FSetAVL]
Raw.create [definition, in Coq.FSets.FSetAVL]
Raw.create [definition, in Coq.FSets.FMapAVL]
Raw.diff [definition, in Coq.FSets.FSetWeakList]
Raw.diff [definition, in Coq.FSets.FSetList]
Raw.diff [definition, in Coq.FSets.FSetAVL]
Raw.diff_Inf [lemma, in Coq.FSets.FSetList]
Raw.diff_sort [lemma, in Coq.FSets.FSetList]
Raw.diff_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.diff_0 [lemma, in Coq.FSets.FSetWeakList]
Raw.diff_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.diff_1 [lemma, in Coq.FSets.FSetList]
Raw.diff_2 [lemma, in Coq.FSets.FSetList]
Raw.diff_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.diff_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.diff_3 [lemma, in Coq.FSets.FSetList]
Raw.elements [definition, in Coq.FSets.FMapWeakList]
Raw.elements [definition, in Coq.FSets.FSetAVL]
Raw.elements [definition, in Coq.FSets.FMapList]
Raw.elements [definition, in Coq.FSets.FMapAVL]
Raw.elements [definition, in Coq.FSets.FSetWeakList]
Raw.elements [definition, in Coq.FSets.FSetList]
Raw.elements_aux [definition, in Coq.FSets.FSetAVL]
Raw.elements_aux [definition, in Coq.FSets.FMapAVL]
Raw.elements_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.elements_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.elements_1 [lemma, in Coq.FSets.FMapList]
Raw.elements_1 [lemma, in Coq.FSets.FSetList]
Raw.elements_2 [lemma, in Coq.FSets.FMapList]
Raw.elements_2 [lemma, in Coq.FSets.FSetList]
Raw.elements_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.elements_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.elements_3 [lemma, in Coq.FSets.FSetList]
Raw.elements_3 [lemma, in Coq.FSets.FMapList]
Raw.elements_3w [lemma, in Coq.FSets.FMapWeakList]
Raw.elements_3w [lemma, in Coq.FSets.FMapList]
Raw.elements_3w [lemma, in Coq.FSets.FSetWeakList]
Raw.elements_3w [lemma, in Coq.FSets.FSetList]
Raw.elt [definition, in Coq.FSets.FSetAVL]
Raw.Elt [section, in Coq.FSets.FMapList]
Raw.Elt [section, in Coq.FSets.FMapWeakList]
Raw.elt [definition, in Coq.FSets.FSetWeakList]
Raw.elt [definition, in Coq.FSets.FSetList]
Raw.Elt [section, in Coq.FSets.FMapAVL]
Raw.Elt.cmp [variable, in Coq.FSets.FMapAVL]
Raw.Elt.elt [variable, in Coq.FSets.FMapWeakList]
Raw.Elt.elt [variable, in Coq.FSets.FMapAVL]
Raw.Elt.elt [variable, in Coq.FSets.FMapList]
Raw.Elt.elt' [variable, in Coq.FSets.FMapWeakList]
Raw.Elt.elt' [variable, in Coq.FSets.FMapList]
Raw.Elt2 [section, in Coq.FSets.FMapWeakList]
Raw.Elt2 [section, in Coq.FSets.FMapList]
Raw.Elt2.elt [variable, in Coq.FSets.FMapWeakList]
Raw.Elt2.elt [variable, in Coq.FSets.FMapList]
Raw.Elt2.elt' [variable, in Coq.FSets.FMapWeakList]
Raw.Elt2.elt' [variable, in Coq.FSets.FMapList]
Raw.Elt3 [section, in Coq.FSets.FMapWeakList]
Raw.Elt3 [section, in Coq.FSets.FMapList]
Raw.Elt3.elt [variable, in Coq.FSets.FMapWeakList]
Raw.Elt3.elt [variable, in Coq.FSets.FMapList]
Raw.Elt3.elt' [variable, in Coq.FSets.FMapWeakList]
Raw.Elt3.elt' [variable, in Coq.FSets.FMapList]
Raw.Elt3.elt'' [variable, in Coq.FSets.FMapList]
Raw.Elt3.elt'' [variable, in Coq.FSets.FMapWeakList]
Raw.Elt3.f [variable, in Coq.FSets.FMapList]
Raw.Elt3.f [variable, in Coq.FSets.FMapWeakList]
Raw.Empty [definition, in Coq.FSets.FSetWeakList]
Raw.Empty [definition, in Coq.FSets.FMapWeakList]
Raw.empty [definition, in Coq.FSets.FMapWeakList]
Raw.empty [definition, in Coq.FSets.FMapList]
Raw.empty [definition, in Coq.FSets.FSetList]
Raw.empty [definition, in Coq.FSets.FMapAVL]
Raw.Empty [definition, in Coq.FSets.FSetList]
Raw.empty [definition, in Coq.FSets.FSetAVL]
Raw.Empty [definition, in Coq.FSets.FSetAVL]
Raw.Empty [definition, in Coq.FSets.FMapList]
Raw.empty [definition, in Coq.FSets.FSetWeakList]
Raw.empty_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.empty_sort [lemma, in Coq.FSets.FSetList]
Raw.empty_sorted [lemma, in Coq.FSets.FMapList]
Raw.empty_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.empty_1 [lemma, in Coq.FSets.FMapList]
Raw.empty_1 [lemma, in Coq.FSets.FSetList]
Raw.empty_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.empty_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.End [constructor, in Coq.FSets.FSetAVL]
Raw.End [constructor, in Coq.FSets.FMapAVL]
Raw.enumeration [inductive, in Coq.FSets.FSetAVL]
Raw.enumeration [inductive, in Coq.FSets.FMapAVL]
Raw.eq [definition, in Coq.FSets.FSetList]
Raw.eq [definition, in Coq.FSets.FSetWeakList]
Raw.eqk [abbreviation, in Coq.FSets.FMapWeakList]
Raw.eqk [abbreviation, in Coq.FSets.FMapList]
Raw.eqke [abbreviation, in Coq.FSets.FMapList]
Raw.eqke [abbreviation, in Coq.FSets.FMapWeakList]
Raw.Equal [definition, in Coq.FSets.FSetList]
Raw.Equal [definition, in Coq.FSets.FSetAVL]
Raw.equal [definition, in Coq.FSets.FMapAVL]
Raw.Equal [definition, in Coq.FSets.FSetWeakList]
Raw.equal [definition, in Coq.FSets.FSetAVL]
Raw.equal [definition, in Coq.FSets.FSetList]
Raw.equal [definition, in Coq.FSets.FMapWeakList]
Raw.equal [definition, in Coq.FSets.FSetWeakList]
Raw.equal_cons [lemma, in Coq.FSets.FMapList]
Raw.equal_cont [definition, in Coq.FSets.FMapAVL]
Raw.equal_end [definition, in Coq.FSets.FMapAVL]
Raw.equal_more [definition, in Coq.FSets.FMapAVL]
Raw.equal_1 [lemma, in Coq.FSets.FMapList]
Raw.equal_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.equal_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.equal_1 [lemma, in Coq.FSets.FSetList]
Raw.equal_2 [lemma, in Coq.FSets.FSetList]
Raw.equal_2 [lemma, in Coq.FSets.FMapList]
Raw.equal_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.equal_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.Equivb [definition, in Coq.FSets.FMapWeakList]
Raw.Equivb [definition, in Coq.FSets.FMapList]
Raw.eq_dec [definition, in Coq.FSets.FSetWeakList]
Raw.eq_refl [lemma, in Coq.FSets.FSetWeakList]
Raw.eq_refl [lemma, in Coq.FSets.FSetList]
Raw.eq_sym [lemma, in Coq.FSets.FSetList]
Raw.eq_sym [lemma, in Coq.FSets.FSetWeakList]
Raw.eq_trans [lemma, in Coq.FSets.FSetList]
Raw.eq_trans [lemma, in Coq.FSets.FSetWeakList]
Raw.Exists [definition, in Coq.FSets.FSetAVL]
Raw.Exists [definition, in Coq.FSets.FSetList]
Raw.Exists [definition, in Coq.FSets.FSetWeakList]
Raw.exists_ [definition, in Coq.FSets.FSetList]
Raw.exists_ [definition, in Coq.FSets.FSetAVL]
Raw.exists_ [definition, in Coq.FSets.FSetWeakList]
Raw.exists_1 [lemma, in Coq.FSets.FSetList]
Raw.exists_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.exists_2 [lemma, in Coq.FSets.FSetList]
Raw.exists_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.filter [definition, in Coq.FSets.FSetList]
Raw.filter [definition, in Coq.FSets.FSetWeakList]
Raw.filter [definition, in Coq.FSets.FSetAVL]
Raw.filter_acc [definition, in Coq.FSets.FSetAVL]
Raw.filter_Inf [lemma, in Coq.FSets.FSetList]
Raw.filter_sort [lemma, in Coq.FSets.FSetList]
Raw.filter_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.filter_1 [lemma, in Coq.FSets.FSetList]
Raw.filter_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.filter_2 [lemma, in Coq.FSets.FSetList]
Raw.filter_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.filter_3 [lemma, in Coq.FSets.FSetList]
Raw.filter_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.find [definition, in Coq.FSets.FMapAVL]
Raw.find_eq [lemma, in Coq.FSets.FMapWeakList]
Raw.find_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.find_1 [lemma, in Coq.FSets.FMapList]
Raw.find_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.find_2 [lemma, in Coq.FSets.FMapList]
Raw.fold [definition, in Coq.FSets.FMapAVL]
Raw.fold [definition, in Coq.FSets.FSetWeakList]
Raw.fold [definition, in Coq.FSets.FSetList]
Raw.fold [definition, in Coq.FSets.FSetAVL]
Raw.fold_right_pair [definition, in Coq.FSets.FMapWeakList]
Raw.fold_right_pair [definition, in Coq.FSets.FMapList]
Raw.fold_right_pair_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.fold_1 [lemma, in Coq.FSets.FSetList]
Raw.fold_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.fold_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.fold_1 [lemma, in Coq.FSets.FMapList]
Raw.ForNotations [section, in Coq.FSets.FSetWeakList]
Raw.ForNotations [section, in Coq.FSets.FSetList]
Raw.For_all [definition, in Coq.FSets.FSetWeakList]
Raw.For_all [definition, in Coq.FSets.FSetAVL]
Raw.for_all [definition, in Coq.FSets.FSetAVL]
Raw.For_all [definition, in Coq.FSets.FSetList]
Raw.for_all [definition, in Coq.FSets.FSetWeakList]
Raw.for_all [definition, in Coq.FSets.FSetList]
Raw.for_all_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.for_all_1 [lemma, in Coq.FSets.FSetList]
Raw.for_all_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.for_all_2 [lemma, in Coq.FSets.FSetList]
Raw.gt_tree [definition, in Coq.FSets.FMapAVL]
Raw.gt_tree [definition, in Coq.FSets.FSetAVL]
Raw.height [definition, in Coq.FSets.FMapAVL]
Raw.height [definition, in Coq.FSets.FSetAVL]
Raw.In [abbreviation, in Coq.FSets.FSetList]
Raw.In [inductive, in Coq.FSets.FMapAVL]
Raw.In [inductive, in Coq.FSets.FSetAVL]
Raw.In [abbreviation, in Coq.FSets.FMapWeakList]
Raw.In [abbreviation, in Coq.FSets.FSetWeakList]
Raw.In [abbreviation, in Coq.FSets.FMapList]
Raw.Inf [abbreviation, in Coq.FSets.FSetList]
Raw.Inf [abbreviation, in Coq.FSets.FMapList]
Raw.InLeft [constructor, in Coq.FSets.FMapAVL]
Raw.InLeft [constructor, in Coq.FSets.FSetAVL]
Raw.InRight [constructor, in Coq.FSets.FMapAVL]
Raw.InRight [constructor, in Coq.FSets.FSetAVL]
Raw.InRoot [constructor, in Coq.FSets.FMapAVL]
Raw.inter [definition, in Coq.FSets.FSetAVL]
Raw.inter [definition, in Coq.FSets.FSetWeakList]
Raw.inter [definition, in Coq.FSets.FSetList]
Raw.inter_Inf [lemma, in Coq.FSets.FSetList]
Raw.inter_sort [lemma, in Coq.FSets.FSetList]
Raw.inter_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.inter_0 [lemma, in Coq.FSets.FSetWeakList]
Raw.inter_1 [lemma, in Coq.FSets.FSetList]
Raw.inter_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.inter_2 [lemma, in Coq.FSets.FSetList]
Raw.inter_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.inter_3 [lemma, in Coq.FSets.FSetList]
Raw.inter_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.Invariants [section, in Coq.FSets.FMapAVL]
Raw.Invariants.elt [variable, in Coq.FSets.FMapAVL]
Raw.In0 [definition, in Coq.FSets.FMapAVL]
Raw.In_eq [lemma, in Coq.FSets.FSetWeakList]
Raw.IsRoot [constructor, in Coq.FSets.FSetAVL]
Raw.is_empty [definition, in Coq.FSets.FSetWeakList]
Raw.is_empty [definition, in Coq.FSets.FSetAVL]
Raw.is_empty [definition, in Coq.FSets.FMapWeakList]
Raw.is_empty [definition, in Coq.FSets.FSetList]
Raw.is_empty [definition, in Coq.FSets.FMapAVL]
Raw.is_empty [definition, in Coq.FSets.FMapList]
Raw.is_empty_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.is_empty_1 [lemma, in Coq.FSets.FSetList]
Raw.is_empty_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.is_empty_1 [lemma, in Coq.FSets.FMapList]
Raw.is_empty_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.is_empty_2 [lemma, in Coq.FSets.FMapList]
Raw.is_empty_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.is_empty_2 [lemma, in Coq.FSets.FSetList]
Raw.join [definition, in Coq.FSets.FMapAVL]
Raw.join [definition, in Coq.FSets.FSetAVL]
Raw.key [definition, in Coq.FSets.FMapAVL]
Raw.key [definition, in Coq.FSets.FMapWeakList]
Raw.key [definition, in Coq.FSets.FMapList]
Raw.Leaf [constructor, in Coq.FSets.FMapAVL]
Raw.Leaf [constructor, in Coq.FSets.FSetAVL]
Raw.lt [inductive, in Coq.FSets.FSetList]
Raw.ltk [abbreviation, in Coq.FSets.FMapList]
Raw.lt_cons_eq [constructor, in Coq.FSets.FSetList]
Raw.lt_cons_lt [constructor, in Coq.FSets.FSetList]
Raw.lt_nil [constructor, in Coq.FSets.FSetList]
Raw.lt_not_eq [lemma, in Coq.FSets.FSetList]
Raw.lt_trans [lemma, in Coq.FSets.FSetList]
Raw.lt_tree [definition, in Coq.FSets.FSetAVL]
Raw.lt_tree [definition, in Coq.FSets.FMapAVL]
Raw.map [definition, in Coq.FSets.FMapWeakList]
Raw.map [definition, in Coq.FSets.FMapList]
Raw.map [definition, in Coq.FSets.FMapAVL]
Raw.mapi [definition, in Coq.FSets.FMapAVL]
Raw.mapi [definition, in Coq.FSets.FMapWeakList]
Raw.mapi [definition, in Coq.FSets.FMapList]
Raw.mapi_lelistA [lemma, in Coq.FSets.FMapList]
Raw.mapi_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.mapi_sorted [lemma, in Coq.FSets.FMapList]
Raw.mapi_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.mapi_1 [lemma, in Coq.FSets.FMapList]
Raw.mapi_2 [lemma, in Coq.FSets.FMapList]
Raw.mapi_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.MapsLeft [constructor, in Coq.FSets.FMapAVL]
Raw.MapsRight [constructor, in Coq.FSets.FMapAVL]
Raw.MapsRoot [constructor, in Coq.FSets.FMapAVL]
Raw.MapsTo [abbreviation, in Coq.FSets.FMapList]
Raw.MapsTo [inductive, in Coq.FSets.FMapAVL]
Raw.MapsTo [abbreviation, in Coq.FSets.FMapWeakList]
Raw.map2 [definition, in Coq.FSets.FMapAVL]
Raw.map2 [definition, in Coq.FSets.FMapList]
Raw.map2 [definition, in Coq.FSets.FMapWeakList]
Raw.Map2 [section, in Coq.FSets.FMapAVL]
Raw.Map2.elt [variable, in Coq.FSets.FMapAVL]
Raw.Map2.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Map2.elt'' [variable, in Coq.FSets.FMapAVL]
Raw.Map2.f [variable, in Coq.FSets.FMapAVL]
Raw.map2_alt [definition, in Coq.FSets.FMapList]
Raw.map2_alt_equiv [lemma, in Coq.FSets.FMapList]
Raw.map2_l [definition, in Coq.FSets.FMapList]
Raw.map2_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.Map2_opt [section, in Coq.FSets.FMapAVL]
Raw.map2_opt [definition, in Coq.FSets.FMapAVL]
Raw.Map2_opt.elt [variable, in Coq.FSets.FMapAVL]
Raw.Map2_opt.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Map2_opt.elt'' [variable, in Coq.FSets.FMapAVL]
Raw.Map2_opt.f [variable, in Coq.FSets.FMapAVL]
Raw.Map2_opt.mapl [variable, in Coq.FSets.FMapAVL]
Raw.Map2_opt.mapr [variable, in Coq.FSets.FMapAVL]
Raw.map2_r [definition, in Coq.FSets.FMapList]
Raw.map2_sorted [lemma, in Coq.FSets.FMapList]
Raw.map2_0 [lemma, in Coq.FSets.FMapWeakList]
Raw.map2_0 [lemma, in Coq.FSets.FMapList]
Raw.map2_1 [lemma, in Coq.FSets.FMapList]
Raw.map2_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.map2_2 [lemma, in Coq.FSets.FMapList]
Raw.map2_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.map_lelistA [lemma, in Coq.FSets.FMapList]
Raw.map_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.map_option [definition, in Coq.FSets.FMapAVL]
Raw.map_sorted [lemma, in Coq.FSets.FMapList]
Raw.map_1 [lemma, in Coq.FSets.FMapList]
Raw.map_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.map_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.map_2 [lemma, in Coq.FSets.FMapList]
Raw.max_elt [definition, in Coq.FSets.FSetList]
Raw.max_elt [definition, in Coq.FSets.FSetAVL]
Raw.max_elt_1 [lemma, in Coq.FSets.FSetList]
Raw.max_elt_2 [lemma, in Coq.FSets.FSetList]
Raw.max_elt_3 [lemma, in Coq.FSets.FSetList]
Raw.mem [definition, in Coq.FSets.FSetWeakList]
Raw.mem [definition, in Coq.FSets.FSetAVL]
Raw.mem [definition, in Coq.FSets.FSetList]
Raw.mem [definition, in Coq.FSets.FMapAVL]
Raw.mem_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.mem_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.mem_1 [lemma, in Coq.FSets.FMapList]
Raw.mem_1 [lemma, in Coq.FSets.FSetList]
Raw.mem_2 [lemma, in Coq.FSets.FMapList]
Raw.mem_2 [lemma, in Coq.FSets.FSetList]
Raw.mem_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.mem_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.merge [definition, in Coq.FSets.FMapAVL]
Raw.merge [definition, in Coq.FSets.FSetAVL]
Raw.min_elt [definition, in Coq.FSets.FSetAVL]
Raw.min_elt [definition, in Coq.FSets.FSetList]
Raw.min_elt_1 [lemma, in Coq.FSets.FSetList]
Raw.min_elt_2 [lemma, in Coq.FSets.FSetList]
Raw.min_elt_3 [lemma, in Coq.FSets.FSetList]
Raw.mktriple [constructor, in Coq.FSets.FSetAVL]
Raw.mktriple [constructor, in Coq.FSets.FMapAVL]
Raw.More [constructor, in Coq.FSets.FSetAVL]
Raw.More [constructor, in Coq.FSets.FMapAVL]
Raw.Node [constructor, in Coq.FSets.FMapAVL]
Raw.Node [constructor, in Coq.FSets.FSetAVL]
Raw.NoDup [abbreviation, in Coq.FSets.FSetWeakList]
Raw.NoDupA [abbreviation, in Coq.FSets.FMapWeakList]
Raw.oee' [abbreviation, in Coq.FSets.FMapList]
Raw.oee' [abbreviation, in Coq.FSets.FMapWeakList]
Raw.option_cons [definition, in Coq.FSets.FMapList]
Raw.option_cons [definition, in Coq.FSets.FMapWeakList]
Raw.partition [definition, in Coq.FSets.FSetWeakList]
Raw.partition [definition, in Coq.FSets.FSetAVL]
Raw.partition [definition, in Coq.FSets.FSetList]
Raw.partition_acc [definition, in Coq.FSets.FSetAVL]
Raw.partition_aux_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_aux_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_Inf_1 [lemma, in Coq.FSets.FSetList]
Raw.partition_Inf_2 [lemma, in Coq.FSets.FSetList]
Raw.partition_sort_1 [lemma, in Coq.FSets.FSetList]
Raw.partition_sort_2 [lemma, in Coq.FSets.FSetList]
Raw.partition_unique_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_unique_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_1 [lemma, in Coq.FSets.FSetList]
Raw.partition_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.partition_2 [lemma, in Coq.FSets.FSetList]
Raw.Proofs.add_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.add_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.add_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.add_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.add_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.add_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.add_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.add_3 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.bal_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.bal_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.bal_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.bal_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.bal_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.bal_mapsto [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.choose_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.choose_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.choose_3 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.Cmp [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.compare_Cmp [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.compare_cont_Cmp [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.compare_end_Cmp [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.compare_more_Cmp [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.concat_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.concat_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.concat_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.concat_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.concat_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.cons_Cmp [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.cons_IfEq [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.cons_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.cons_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.create_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.create_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.create_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.create_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.diff_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.diff_bst_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.diff_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_app [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_app [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_cardinal [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_aux_cardinal [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_aux_mapsto [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_sort [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_sort [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_cardinal [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_cardinal [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_mapsto [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_node [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_node [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_nodup [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.elements_nodup [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_sort [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.elements_sort [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.Elt [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Elt.cmp [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Elt.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Empty [definition, in Coq.FSets.FMapAVL]
Raw.Proofs.empty_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.empty_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.empty_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.empty_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.eq [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.eqk [abbreviation, in Coq.FSets.FMapAVL]
Raw.Proofs.eqke [abbreviation, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_cont_IfEq [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_end_IfEq [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_Equivb [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_IfEq [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_more_IfEq [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.equal_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.equal_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.Equivb [definition, in Coq.FSets.FMapAVL]
Raw.Proofs.Equivb_elements [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.eq_L_eq [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.eq_refl [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.eq_sym [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.eq_trans [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.exists_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.exists_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.F [section, in Coq.FSets.FSetAVL]
Raw.Proofs.filter_acc_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.filter_acc_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.filter_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.filter_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.find_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_iff [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_in_equiv [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_in_iff [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_mapsto_equiv [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.find_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e [definition, in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.flatten_e_elements [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e_elements [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.fold' [definition, in Coq.FSets.FMapAVL]
Raw.Proofs.fold' [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.fold_equiv [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.fold_equiv [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.fold_equiv_aux [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.fold_equiv_aux [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.fold_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.fold_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.for_all_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.for_all_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.F.f [variable, in Coq.FSets.FSetAVL]
Raw.Proofs.gt_leaf [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_leaf [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.gt_left [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_right [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_node [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_node [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.gt_tree_not_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_not_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.gt_tree_trans [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_trans [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.IfEq [definition, in Coq.FSets.FMapAVL]
Raw.Proofs.inter_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.inter_bst_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.inter_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.In_alt [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.in_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.In_MapsTo [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.In_node_iff [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.In_node_iff [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.In_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.In_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.is_empty_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.is_empty_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.is_empty_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.is_empty_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.join_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.join_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.join_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.join_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.join_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.ltk [abbreviation, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_leaf [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_leaf [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_left [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_not_eq [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_right [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_trans [definition, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_tree_node [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_tree_node [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_tree_not_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.lt_tree_not_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_tree_trans [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.lt_tree_trans [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.L_eq_cons [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.L_eq_eq [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.Map [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Mapi [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Mapi.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Mapi.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Mapi.f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.MapsTo_In [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.MapsTo_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.Map.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map.f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2 [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2.elt'' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2.f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt [abbreviation, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.elt'' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.f0 [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.f0_compat [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.f0_f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapl [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapl_bst [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapl_f0 [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapr [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapr_bst [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map2_opt.mapr_f0 [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map2_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.Map_option [section, in Coq.FSets.FMapAVL]
Raw.Proofs.Map_option.elt [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map_option.elt' [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map_option.f [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.Map_option.f_compat [variable, in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.map_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.max_elt_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.max_elt_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.max_elt_3 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.mem_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.mem_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.mem_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.mem_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.merge_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.merge_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.merge_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.merge_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.merge_mapsto [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.min_elt_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.min_elt_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.min_elt_3 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.not_find_iff [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.partition_acc_bst_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_acc_bst_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_acc_in_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_acc_in_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_bst_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_bst_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_in_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.partition_in_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_min_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_min_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_gt_tree [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_gt_tree [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_min_in [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.remove_min_in [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_mapsto [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.remove_3 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.singleton_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.singleton_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.singleton_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.split_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.split_bst [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_find [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_gt_tree [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_1 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.split_in_1 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_2 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.split_in_2 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_3 [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_3 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.split_lt_tree [lemma, in Coq.FSets.FMapAVL]
Raw.Proofs.subsetl_12 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.subsetr_12 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.subset_12 [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.union_bst [lemma, in Coq.FSets.FSetAVL]
Raw.Proofs.union_in [lemma, in Coq.FSets.FSetAVL]
Raw.remove [definition, in Coq.FSets.FSetList]
Raw.remove [definition, in Coq.FSets.FMapAVL]
Raw.remove [definition, in Coq.FSets.FSetWeakList]
Raw.remove [definition, in Coq.FSets.FSetAVL]
Raw.remove_Inf [lemma, in Coq.FSets.FSetList]
Raw.remove_Inf [lemma, in Coq.FSets.FMapList]
Raw.remove_min [definition, in Coq.FSets.FMapAVL]
Raw.remove_min [definition, in Coq.FSets.FSetAVL]
Raw.remove_NoDup [lemma, in Coq.FSets.FMapWeakList]
Raw.remove_sort [lemma, in Coq.FSets.FSetList]
Raw.remove_sorted [lemma, in Coq.FSets.FMapList]
Raw.remove_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.remove_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.remove_1 [lemma, in Coq.FSets.FMapList]
Raw.remove_1 [lemma, in Coq.FSets.FSetList]
Raw.remove_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.remove_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.remove_2 [lemma, in Coq.FSets.FMapList]
Raw.remove_2 [lemma, in Coq.FSets.FSetList]
Raw.remove_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.remove_3 [lemma, in Coq.FSets.FSetList]
Raw.remove_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.remove_3 [lemma, in Coq.FSets.FMapList]
Raw.remove_3 [lemma, in Coq.FSets.FMapWeakList]
Raw.remove_3' [lemma, in Coq.FSets.FMapWeakList]
Raw.singleton [definition, in Coq.FSets.FSetAVL]
Raw.singleton [definition, in Coq.FSets.FSetWeakList]
Raw.singleton [definition, in Coq.FSets.FSetList]
Raw.singleton_sort [lemma, in Coq.FSets.FSetList]
Raw.singleton_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.singleton_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.singleton_1 [lemma, in Coq.FSets.FSetList]
Raw.singleton_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.singleton_2 [lemma, in Coq.FSets.FSetList]
Raw.Sort [abbreviation, in Coq.FSets.FSetList]
Raw.Sort [abbreviation, in Coq.FSets.FMapList]
Raw.split [definition, in Coq.FSets.FMapAVL]
Raw.split [definition, in Coq.FSets.FSetAVL]
Raw.submap [definition, in Coq.FSets.FMapWeakList]
Raw.Submap [definition, in Coq.FSets.FMapWeakList]
Raw.submap_1 [lemma, in Coq.FSets.FMapWeakList]
Raw.submap_2 [lemma, in Coq.FSets.FMapWeakList]
Raw.subset [definition, in Coq.FSets.FSetAVL]
Raw.Subset [definition, in Coq.FSets.FSetList]
Raw.Subset [definition, in Coq.FSets.FSetAVL]
Raw.Subset [definition, in Coq.FSets.FSetWeakList]
Raw.subset [definition, in Coq.FSets.FSetWeakList]
Raw.subset [definition, in Coq.FSets.FSetList]
Raw.subsetl [definition, in Coq.FSets.FSetAVL]
Raw.subsetr [definition, in Coq.FSets.FSetAVL]
Raw.subset_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.subset_1 [lemma, in Coq.FSets.FSetList]
Raw.subset_2 [lemma, in Coq.FSets.FSetList]
Raw.subset_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.t [abbreviation, in Coq.FSets.FMapAVL]
Raw.t [abbreviation, in Coq.FSets.FSetAVL]
Raw.t [definition, in Coq.FSets.FSetList]
Raw.t [abbreviation, in Coq.FSets.FMapAVL]
Raw.t [definition, in Coq.FSets.FSetWeakList]
Raw.t [definition, in Coq.FSets.FMapList]
Raw.t [definition, in Coq.FSets.FMapWeakList]
Raw.tree [inductive, in Coq.FSets.FMapAVL]
Raw.tree [inductive, in Coq.FSets.FSetAVL]
Raw.triple [record, in Coq.FSets.FMapAVL]
Raw.triple [record, in Coq.FSets.FSetAVL]
Raw.t_in [projection, in Coq.FSets.FSetAVL]
Raw.t_left [projection, in Coq.FSets.FMapAVL]
Raw.t_left [projection, in Coq.FSets.FSetAVL]
Raw.t_opt [projection, in Coq.FSets.FMapAVL]
Raw.t_right [projection, in Coq.FSets.FSetAVL]
Raw.t_right [projection, in Coq.FSets.FMapAVL]
Raw.union [definition, in Coq.FSets.FSetWeakList]
Raw.union [definition, in Coq.FSets.FSetList]
Raw.union [definition, in Coq.FSets.FSetAVL]
Raw.union_Inf [lemma, in Coq.FSets.FSetList]
Raw.union_sort [lemma, in Coq.FSets.FSetList]
Raw.union_unique [lemma, in Coq.FSets.FSetWeakList]
Raw.union_0 [lemma, in Coq.FSets.FSetWeakList]
Raw.union_1 [lemma, in Coq.FSets.FSetList]
Raw.union_1 [lemma, in Coq.FSets.FSetWeakList]
Raw.union_2 [lemma, in Coq.FSets.FSetWeakList]
Raw.union_2 [lemma, in Coq.FSets.FSetList]
Raw.union_3 [lemma, in Coq.FSets.FSetWeakList]
Raw.union_3 [lemma, in Coq.FSets.FSetList]
Raxioms [library]
Rbase [library]
Rbasic_fun [library]
Rcase_abs [lemma, in Coq.Reals.Rbasic_fun]
Rcomplete [library]
Rcontinuity_abs [lemma, in Coq.Reals.Ranalysis4]
Rdefinitions [library]
Rderiv [library]
Rderivable_pt_abs [lemma, in Coq.Reals.Ranalysis4]
Rdichotomy [lemma, in Coq.Reals.RIneq]
Rdiv [definition, in Coq.Reals.Rdefinitions]
Reals [library]
rec [projection, in Coq.Program.Equality]
recl [definition, in Coq.Numbers.Cyclic.Int31.Int31]
recl_aux [definition, in Coq.Numbers.Cyclic.Int31.Int31]
recr [definition, in Coq.Numbers.Cyclic.Int31.Int31]
recrbis [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recrbis_aux [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recrbis_aux_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recrbis_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_aux [definition, in Coq.Numbers.Cyclic.Int31.Int31]
recr_aux_converges [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_aux_eqn [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_eqn [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Recursor [record, in Coq.Program.Equality]
rec_type [projection, in Coq.Program.Equality]
Reduce [section, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec [section, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec.c [variable, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec.nT [variable, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec.N0 [variable, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec.reduce_1n [variable, in Coq.Numbers.Natural.BigN.Nbasic]
ReduceRec.w [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.eq0 [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.nT [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.N0 [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.reduce_n [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.w [variable, in Coq.Numbers.Natural.BigN.Nbasic]
Reduce.zn2z_to_Nt [variable, in Coq.Numbers.Natural.BigN.Nbasic]
reduce_n [definition, in Coq.Numbers.Natural.BigN.Nbasic]
reduce_n1 [definition, in Coq.Numbers.Natural.BigN.Nbasic]
ReDun [section, in Coq.Lists.List]
ReDun.A [variable, in Coq.Lists.List]
Reflexive [definition, in Coq.Sets.Relations_1]
reflexive [definition, in Coq.Relations.Relation_Definitions]
Reflexive [record, in Coq.Classes.RelationClasses]
Reflexive [inductive, in Coq.Classes.RelationClasses]
Reflexive_complement_Irreflexive [instance, in Coq.Classes.RelationClasses]
reflexive_eq_dom_reflexive [instance, in Coq.Classes.Morphisms]
reflexive_morphism [lemma, in Coq.Classes.Morphisms]
reflexive_morphism_proxy [instance, in Coq.Classes.Morphisms]
Reflexive_partial_app_morphism [lemma, in Coq.Classes.Morphisms]
Reflexive_Symetric_Transitive_Closure [section, in Coq.Relations.Relation_Operators]
Reflexive_Symetric_Transitive_Closure.A [variable, in Coq.Relations.Relation_Operators]
Reflexive_Symetric_Transitive_Closure.R [variable, in Coq.Relations.Relation_Operators]
Reflexive_Transitive_Closure [section, in Coq.Relations.Relation_Operators]
Reflexive_Transitive_Closure.A [variable, in Coq.Relations.Relation_Operators]
Reflexive_Transitive_Closure.R [variable, in Coq.Relations.Relation_Operators]
reflexivity [projection, in Coq.Classes.RelationClasses]
reflexivity [constructor, in Coq.Classes.RelationClasses]
refl_equal [constructor, in Coq.Init.Logic]
refl_identity [constructor, in Coq.Init.Datatypes]
Rel [definition, in Coq.Sets.Partial_Order]
Relation [definition, in Coq.Sets.Relations_1]
relation [definition, in Coq.Relations.Relation_Definitions]
RelationalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
RelationalChoice [library]
RelationalChoice_on [definition, in Coq.Logic.ChoiceFacts]
relational_choice [axiom, in Coq.Logic.RelationalChoice]
RelationClasses [library]
RelationOnProduct [section, in Coq.Numbers.NumPrelude]
RelationOnProduct.A [variable, in Coq.Numbers.NumPrelude]
RelationOnProduct.Aeq [variable, in Coq.Numbers.NumPrelude]
RelationOnProduct.B [variable, in Coq.Numbers.NumPrelude]
RelationOnProduct.Beq [variable, in Coq.Numbers.NumPrelude]
RelationOnProduct.EA_equiv [variable, in Coq.Numbers.NumPrelude]
RelationOnProduct.EB_equiv [variable, in Coq.Numbers.NumPrelude]
Relations [library]
relations_eq [definition, in Coq.Numbers.NumPrelude]
relations_eq_equiv [lemma, in Coq.Numbers.NumPrelude]
Relations_1 [section, in Coq.Sets.Relations_1]
Relations_1 [library]
Relations_1.R [variable, in Coq.Sets.Relations_1]
Relations_1.U [variable, in Coq.Sets.Relations_1]
Relations_1_facts [library]
Relations_2 [section, in Coq.Sets.Relations_2]
Relations_2 [library]
Relations_2.R [variable, in Coq.Sets.Relations_2]
Relations_2.U [variable, in Coq.Sets.Relations_2]
Relations_2_facts [library]
Relations_3 [section, in Coq.Sets.Relations_3]
Relations_3 [library]
Relations_3.R [variable, in Coq.Sets.Relations_3]
Relations_3.U [variable, in Coq.Sets.Relations_3]
Relations_3_facts [library]
relation_conjunction [definition, in Coq.Classes.RelationClasses]
relation_conjunction_morphism [instance, in Coq.Classes.Morphisms_Relations]
Relation_Definition [section, in Coq.Relations.Relation_Definitions]
Relation_Definitions [library]
Relation_Definition.A [variable, in Coq.Relations.Relation_Definitions]
Relation_Definition.General_Properties_of_Relations [section, in Coq.Relations.Relation_Definitions]
Relation_Definition.R [variable, in Coq.Relations.Relation_Definitions]
Relation_Definition.Relations_of_Relations [section, in Coq.Relations.Relation_Definitions]
Relation_Definition.Sets_of_Relations [section, in Coq.Relations.Relation_Definitions]
relation_disjunction [definition, in Coq.Classes.RelationClasses]
relation_disjunction_morphism [instance, in Coq.Classes.Morphisms_Relations]
relation_equivalence [definition, in Coq.Classes.RelationClasses]
relation_equivalence_equivalence [instance, in Coq.Classes.RelationClasses]
relation_equivalence_pointwise [instance, in Coq.Classes.Morphisms_Relations]
relation_implication_preorder [instance, in Coq.Classes.RelationClasses]
Relation_Operators [library]
relation_wd [definition, in Coq.Numbers.NumPrelude]
relative_non_contradiction_of_definite_descr [lemma, in Coq.Logic.ChoiceFacts]
relative_non_contradiction_of_indefinite_descr [lemma, in Coq.Logic.ChoiceFacts]
rel_choice_and_proof_irrel_imp_guarded_rel_choice [lemma, in Coq.Logic.ChoiceFacts]
rel_choice_indep_of_general_premises_imp_guarded_rel_choice [lemma, in Coq.Logic.ChoiceFacts]
Rel_of [projection, in Coq.Sets.Partial_Order]
rel_prime [definition, in Coq.ZArith.Znumtheory]
rel_prime_bezout [lemma, in Coq.ZArith.Znumtheory]
rel_prime_cross_prod [lemma, in Coq.ZArith.Znumtheory]
rel_prime_dec [definition, in Coq.ZArith.Znumtheory]
rel_prime_div [lemma, in Coq.ZArith.Znumtheory]
rel_prime_le_prime [lemma, in Coq.ZArith.Znumtheory]
rel_prime_mod [lemma, in Coq.ZArith.Znumtheory]
rel_prime_mod_rev [lemma, in Coq.ZArith.Znumtheory]
rel_prime_mult [lemma, in Coq.ZArith.Znumtheory]
rel_prime_sym [lemma, in Coq.ZArith.Znumtheory]
rel_prime_Zpower [lemma, in Coq.ZArith.Zpow_facts]
rel_prime_Zpower_r [lemma, in Coq.ZArith.Zpow_facts]
rel_prime_1 [lemma, in Coq.ZArith.Znumtheory]
Remainder [definition, in Coq.ZArith.ZOdiv]
Remainder [definition, in Coq.ZArith.Zdiv]
Remainder_alt [definition, in Coq.ZArith.Zdiv]
Remainder_alt [definition, in Coq.ZArith.ZOdiv]
Remainder_equiv [lemma, in Coq.ZArith.Zdiv]
Remainder_equiv [lemma, in Coq.ZArith.ZOdiv]
remove [definition, in Coq.Lists.List]
removeA [definition, in Coq.Lists.SetoidList]
removeA_equivlistA [lemma, in Coq.Lists.SetoidList]
removeA_filter [lemma, in Coq.Lists.SetoidList]
removeA_InA [lemma, in Coq.Lists.SetoidList]
removeA_NoDupA [lemma, in Coq.Lists.SetoidList]
removelast [definition, in Coq.Lists.List]
removelast_app [lemma, in Coq.Lists.List]
removelast_firstn [lemma, in Coq.Lists.List]
remove_In [lemma, in Coq.Lists.List]
rename [lemma, in Coq.ZArith.Zcompare]
Req_dec [lemma, in Coq.Reals.RIneq]
Req_EM_T [lemma, in Coq.Reals.RiemannInt]
Req_ge [lemma, in Coq.Reals.RIneq]
Req_ge_sym [lemma, in Coq.Reals.RIneq]
Req_le [lemma, in Coq.Reals.RIneq]
Req_le_sym [lemma, in Coq.Reals.RIneq]
respect [projection, in Coq.Classes.Morphisms]
respect [constructor, in Coq.Classes.Morphisms]
respectful [definition, in Coq.Classes.Morphisms]
respectful_hetero [definition, in Coq.Classes.Morphisms]
respectful_morphism [instance, in Coq.Classes.Morphisms]
respectful_per [instance, in Coq.Classes.Morphisms]
respecting [definition, in Coq.Classes.Equivalence]
Respecting [section, in Coq.Classes.Equivalence]
respecting_equiv [instance, in Coq.Classes.Equivalence]
respect_proxy [projection, in Coq.Classes.Morphisms]
respect_proxy [constructor, in Coq.Classes.Morphisms]
Reste [definition, in Coq.Reals.Cos_rel]
Reste1 [definition, in Coq.Reals.Cos_rel]
reste1_cv_R0 [lemma, in Coq.Reals.Cos_plus]
reste1_maj [lemma, in Coq.Reals.Cos_plus]
Reste2 [definition, in Coq.Reals.Cos_rel]
reste2_cv_R0 [lemma, in Coq.Reals.Cos_plus]
reste2_maj [lemma, in Coq.Reals.Cos_plus]
reste_cv_R0 [lemma, in Coq.Reals.Cos_plus]
Reste_E [definition, in Coq.Reals.Exp_prop]
Reste_E_cv [lemma, in Coq.Reals.Exp_prop]
Reste_E_maj [lemma, in Coq.Reals.Exp_prop]
restriction_family [lemma, in Coq.Reals.Rtopology]
retract [record, in Coq.Logic.Berardi]
retract [record, in Coq.Logic.ClassicalFacts]
retract_cond [record, in Coq.Logic.Berardi]
retract_pow_U_U [lemma, in Coq.Logic.Berardi]
rev [definition, in Coq.Lists.List]
rev' [definition, in Coq.Lists.List]
rev_acc [abbreviation, in Coq.Lists.List]
rev_acc_rev [abbreviation, in Coq.Lists.List]
rev_alt [lemma, in Coq.Lists.List]
rev_append [definition, in Coq.Lists.List]
rev_append_rev [lemma, in Coq.Lists.List]
rev_ind [lemma, in Coq.Lists.List]
rev_involutive [lemma, in Coq.Lists.List]
rev_length [lemma, in Coq.Lists.List]
rev_list_ind [lemma, in Coq.Lists.List]
rev_nth [lemma, in Coq.Lists.List]
rev_unit [lemma, in Coq.Lists.List]
RfactN_fact2N_factk [lemma, in Coq.Reals.Rprod]
Rfunctions [library]
Rge [definition, in Coq.Reals.Rdefinitions]
Rgeom [library]
Rge_antisym [lemma, in Coq.Reals.RIneq]
Rge_dec [lemma, in Coq.Reals.RIneq]
Rge_ge_eq [lemma, in Coq.Reals.RIneq]
Rge_gt_dec [lemma, in Coq.Reals.RIneq]
Rge_gt_trans [lemma, in Coq.Reals.RIneq]
Rge_le [lemma, in Coq.Reals.RIneq]
Rge_minus [lemma, in Coq.Reals.RIneq]
Rge_not_gt [lemma, in Coq.Reals.RIneq]
Rge_not_lt [lemma, in Coq.Reals.RIneq]
Rge_or_gt [lemma, in Coq.Reals.RIneq]
Rge_refl [lemma, in Coq.Reals.RIneq]
Rge_trans [lemma, in Coq.Reals.RIneq]
Rgt [definition, in Coq.Reals.Rdefinitions]
Rgt_asym [lemma, in Coq.Reals.RIneq]
Rgt_dec [lemma, in Coq.Reals.RIneq]
Rgt_eq_compat [lemma, in Coq.Reals.RIneq]
Rgt_ge [lemma, in Coq.Reals.RIneq]
Rgt_ge_dec [lemma, in Coq.Reals.RIneq]
Rgt_ge_trans [lemma, in Coq.Reals.RIneq]
Rgt_irrefl [lemma, in Coq.Reals.RIneq]
Rgt_lt [lemma, in Coq.Reals.RIneq]
Rgt_minus [lemma, in Coq.Reals.RIneq]
Rgt_not_eq [lemma, in Coq.Reals.RIneq]
Rgt_not_ge [lemma, in Coq.Reals.RIneq]
Rgt_not_le [lemma, in Coq.Reals.RIneq]
Rgt_or_ge [lemma, in Coq.Reals.RIneq]
Rgt_trans [lemma, in Coq.Reals.RIneq]
Rgt_2PI_0 [lemma, in Coq.Reals.Rtrigo_calc]
Rgt_3PI2_0 [lemma, in Coq.Reals.Rtrigo_calc]
RiemannInt [definition, in Coq.Reals.RiemannInt]
RiemannInt [library]
RiemannInt_exists [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P1 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P10 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P11 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P12 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P13 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P14 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P15 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P16 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P17 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P18 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P19 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P2 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P20 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P21 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P22 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P23 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P24 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P25 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P26 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P27 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P28 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P29 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P3 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P30 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P31 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P32 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P33 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P4 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P5 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P6 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P7 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P8 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_P9 [lemma, in Coq.Reals.RiemannInt]
RiemannInt_SF [definition, in Coq.Reals.RiemannInt_SF]
RiemannInt_SF [library]
Riemann_integrable [definition, in Coq.Reals.RiemannInt]
right [constructor, in Coq.Init.Specif]
RightDistributivityImplicationOverDisjunction [definition, in Coq.Logic.ClassicalFacts]
right_lex [constructor, in Coq.Relations.Relation_Operators]
right_prefix [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
right_sym [constructor, in Coq.Relations.Relation_Operators]
RIneq [library]
Rinv [axiom, in Coq.Reals.Rdefinitions]
RinvN [definition, in Coq.Reals.RiemannInt]
RinvN_cv [lemma, in Coq.Reals.RiemannInt]
RinvN_pos [lemma, in Coq.Reals.RiemannInt]
Rinv_involutive [lemma, in Coq.Reals.RIneq]
Rinv_l [axiom, in Coq.Reals.Raxioms]
Rinv_lt_contravar [lemma, in Coq.Reals.RIneq]
Rinv_lt_0_compat [lemma, in Coq.Reals.RIneq]
Rinv_l_sym [lemma, in Coq.Reals.RIneq]
Rinv_mult_distr [lemma, in Coq.Reals.RIneq]
Rinv_mult_simpl [lemma, in Coq.Reals.RIneq]
Rinv_neq_0_compat [lemma, in Coq.Reals.RIneq]
Rinv_pow [lemma, in Coq.Reals.Rfunctions]
Rinv_r [lemma, in Coq.Reals.RIneq]
Rinv_Rdiv [lemma, in Coq.Reals.Rpower]
Rinv_r_simpl_l [lemma, in Coq.Reals.RIneq]
Rinv_r_simpl_m [lemma, in Coq.Reals.RIneq]
Rinv_r_simpl_r [lemma, in Coq.Reals.RIneq]
Rinv_r_sym [lemma, in Coq.Reals.RIneq]
Rinv_0_lt_compat [lemma, in Coq.Reals.RIneq]
Rinv_1 [lemma, in Coq.Reals.RIneq]
Rinv_1_lt_contravar [lemma, in Coq.Reals.RIneq]
Rle [definition, in Coq.Reals.Rdefinitions]
RLegacyTheory [lemma, in Coq.Reals.LegacyRfield]
Rlength [definition, in Coq.Reals.RList]
Rle_antisym [lemma, in Coq.Reals.RIneq]
Rle_cv_lim [lemma, in Coq.Reals.RiemannInt]
Rle_dec [lemma, in Coq.Reals.RIneq]
Rle_ge [lemma, in Coq.Reals.RIneq]
Rle_le_eq [lemma, in Coq.Reals.RIneq]
Rle_lt_dec [lemma, in Coq.Reals.RIneq]
Rle_lt_or_eq_dec [lemma, in Coq.Reals.RIneq]
Rle_lt_trans [lemma, in Coq.Reals.RIneq]
Rle_lt_0_plus_1 [lemma, in Coq.Reals.RIneq]
Rle_minus [lemma, in Coq.Reals.RIneq]
Rle_not_gt [lemma, in Coq.Reals.RIneq]
Rle_not_lt [lemma, in Coq.Reals.RIneq]
Rle_or_lt [lemma, in Coq.Reals.RIneq]
Rle_pow [lemma, in Coq.Reals.Rfunctions]
Rle_Qle [lemma, in Coq.QArith.Qreals]
Rle_refl [lemma, in Coq.Reals.RIneq]
Rle_Rinv [lemma, in Coq.Reals.Exp_prop]
Rle_Rpower [lemma, in Coq.Reals.Rpower]
Rle_trans [lemma, in Coq.Reals.RIneq]
Rle_0_sqr [lemma, in Coq.Reals.RIneq]
Rle_0_1 [lemma, in Coq.Reals.RIneq]
Rlimit [library]
Rlist [inductive, in Coq.Reals.RList]
RList [library]
RList_P0 [lemma, in Coq.Reals.RList]
RList_P1 [lemma, in Coq.Reals.RList]
Rlist_P1 [lemma, in Coq.Reals.RList]
RList_P10 [lemma, in Coq.Reals.RList]
RList_P11 [lemma, in Coq.Reals.RList]
RList_P12 [lemma, in Coq.Reals.RList]
RList_P13 [lemma, in Coq.Reals.RList]
RList_P14 [lemma, in Coq.Reals.RList]
RList_P15 [lemma, in Coq.Reals.RList]
RList_P16 [lemma, in Coq.Reals.RList]
RList_P17 [lemma, in Coq.Reals.RList]
RList_P18 [lemma, in Coq.Reals.RList]
RList_P19 [lemma, in Coq.Reals.RList]
RList_P2 [lemma, in Coq.Reals.RList]
RList_P20 [lemma, in Coq.Reals.RList]
RList_P21 [lemma, in Coq.Reals.RList]
RList_P22 [lemma, in Coq.Reals.RList]
RList_P23 [lemma, in Coq.Reals.RList]
RList_P24 [lemma, in Coq.Reals.RList]
RList_P25 [lemma, in Coq.Reals.RList]
RList_P26 [lemma, in Coq.Reals.RList]
RList_P27 [lemma, in Coq.Reals.RList]
RList_P28 [lemma, in Coq.Reals.RList]
RList_P29 [lemma, in Coq.Reals.RList]
RList_P3 [lemma, in Coq.Reals.RList]
RList_P4 [lemma, in Coq.Reals.RList]
RList_P5 [lemma, in Coq.Reals.RList]
RList_P6 [lemma, in Coq.Reals.RList]
RList_P7 [lemma, in Coq.Reals.RList]
RList_P8 [lemma, in Coq.Reals.RList]
RList_P9 [lemma, in Coq.Reals.RList]
Rln [definition, in Coq.Reals.Rpower]
Rlogic [library]
Rlt [axiom, in Coq.Reals.Rdefinitions]
Rlt_asym [axiom, in Coq.Reals.Raxioms]
Rlt_dec [lemma, in Coq.Reals.RIneq]
Rlt_dichotomy_converse [lemma, in Coq.Reals.RIneq]
Rlt_eps2_eps [lemma, in Coq.Reals.Rlimit]
Rlt_eps4_eps [lemma, in Coq.Reals.Rlimit]
Rlt_eq_compat [lemma, in Coq.Reals.RIneq]
Rlt_gt [lemma, in Coq.Reals.RIneq]
Rlt_irrefl [lemma, in Coq.Reals.RIneq]
Rlt_le [lemma, in Coq.Reals.RIneq]
Rlt_le_dec [lemma, in Coq.Reals.RIneq]
Rlt_le_trans [lemma, in Coq.Reals.RIneq]
Rlt_minus [lemma, in Coq.Reals.RIneq]
Rlt_not_eq [lemma, in Coq.Reals.RIneq]
Rlt_not_ge [lemma, in Coq.Reals.RIneq]
Rlt_not_le [lemma, in Coq.Reals.RIneq]
Rlt_or_le [lemma, in Coq.Reals.RIneq]
Rlt_PI_3PI2 [lemma, in Coq.Reals.Rtrigo_calc]
Rlt_plus_1 [lemma, in Coq.Reals.RIneq]
Rlt_pow [lemma, in Coq.Reals.Rfunctions]
Rlt_pow_R1 [lemma, in Coq.Reals.Rfunctions]
Rlt_Qlt [lemma, in Coq.QArith.Qreals]
Rlt_Rminus [lemma, in Coq.Reals.Rtopology]
Rlt_R0_R2 [lemma, in Coq.Reals.DiscrR]
Rlt_sqrt2_0 [lemma, in Coq.Reals.Rtrigo_calc]
Rlt_sqrt3_0 [lemma, in Coq.Reals.Rtrigo_calc]
Rlt_trans [axiom, in Coq.Reals.Raxioms]
Rlt_0_sqr [lemma, in Coq.Reals.RIneq]
Rlt_0_1 [lemma, in Coq.Reals.RIneq]
Rlt_3PI2_2PI [lemma, in Coq.Reals.Rtrigo_calc]
Rlt_4 [lemma, in Coq.Reals.Ranalysis2]
Rmax [definition, in Coq.Reals.Rbasic_fun]
RmaxAbs [lemma, in Coq.Reals.Rbasic_fun]
RmaxLess1 [lemma, in Coq.Reals.Rbasic_fun]
RmaxLess2 [lemma, in Coq.Reals.Rbasic_fun]
RmaxRmult [lemma, in Coq.Reals.Rbasic_fun]
RmaxSym [abbreviation, in Coq.Reals.Rbasic_fun]
Rmax_comm [lemma, in Coq.Reals.Rbasic_fun]
Rmax_N [definition, in Coq.Reals.Rseries]
Rmax_Rle [lemma, in Coq.Reals.Rbasic_fun]
Rmax_stable_in_negreal [lemma, in Coq.Reals.Rbasic_fun]
Rmin [definition, in Coq.Reals.Rbasic_fun]
Rminus [definition, in Coq.Reals.Rdefinitions]
Rminus_diag_eq [lemma, in Coq.Reals.RIneq]
Rminus_diag_uniq [lemma, in Coq.Reals.RIneq]
Rminus_diag_uniq_sym [lemma, in Coq.Reals.RIneq]
Rminus_eq_contra [lemma, in Coq.Reals.RIneq]
Rminus_fp1 [lemma, in Coq.Reals.R_Ifp]
Rminus_fp2 [lemma, in Coq.Reals.R_Ifp]
Rminus_ge [lemma, in Coq.Reals.RIneq]
Rminus_gt [lemma, in Coq.Reals.RIneq]
Rminus_Int_part1 [lemma, in Coq.Reals.R_Ifp]
Rminus_Int_part2 [lemma, in Coq.Reals.R_Ifp]
Rminus_le [lemma, in Coq.Reals.RIneq]
Rminus_lt [lemma, in Coq.Reals.RIneq]
Rminus_not_eq [lemma, in Coq.Reals.RIneq]
Rminus_not_eq_right [lemma, in Coq.Reals.RIneq]
Rminus_0_l [lemma, in Coq.Reals.RIneq]
Rminus_0_r [lemma, in Coq.Reals.RIneq]
Rmin_comm [lemma, in Coq.Reals.Rbasic_fun]
Rmin_l [lemma, in Coq.Reals.Rbasic_fun]
Rmin_pos [lemma, in Coq.Reals.Ranalysis2]
Rmin_r [lemma, in Coq.Reals.Rbasic_fun]
Rmin_Rgt [lemma, in Coq.Reals.Rbasic_fun]
Rmin_Rgt_l [lemma, in Coq.Reals.Rbasic_fun]
Rmin_Rgt_r [lemma, in Coq.Reals.Rbasic_fun]
Rmin_stable_in_posreal [lemma, in Coq.Reals.Rbasic_fun]
Rmin_2 [lemma, in Coq.Reals.Ranalysis2]
Rmult [axiom, in Coq.Reals.Rdefinitions]
Rmult_assoc [axiom, in Coq.Reals.Raxioms]
Rmult_comm [axiom, in Coq.Reals.Raxioms]
Rmult_eq_compat_l [lemma, in Coq.Reals.RIneq]
Rmult_eq_reg_l [lemma, in Coq.Reals.RIneq]
Rmult_eq_0_compat [lemma, in Coq.Reals.RIneq]
Rmult_eq_0_compat_l [lemma, in Coq.Reals.RIneq]
Rmult_eq_0_compat_r [lemma, in Coq.Reals.RIneq]
Rmult_ge_compat [lemma, in Coq.Reals.RIneq]
Rmult_ge_compat_l [lemma, in Coq.Reals.RIneq]
Rmult_ge_compat_r [lemma, in Coq.Reals.RIneq]
Rmult_ge_0_gt_0_lt_compat [lemma, in Coq.Reals.RIneq]
Rmult_gt_compat_l [lemma, in Coq.Reals.RIneq]
Rmult_gt_compat_r [lemma, in Coq.Reals.RIneq]
Rmult_gt_reg_l [lemma, in Coq.Reals.RIneq]
Rmult_gt_0_compat [lemma, in Coq.Reals.RIneq]
Rmult_gt_0_lt_compat [lemma, in Coq.Reals.RIneq]
Rmult_integral [lemma, in Coq.Reals.RIneq]
Rmult_integral_contrapositive [lemma, in Coq.Reals.RIneq]
Rmult_integral_contrapositive_currified [lemma, in Coq.Reals.RIneq]
Rmult_le_compat [lemma, in Coq.Reals.RIneq]
Rmult_le_compat_l [lemma, in Coq.Reals.RIneq]
Rmult_le_compat_neg_l [lemma, in Coq.Reals.RIneq]
Rmult_le_compat_r [lemma, in Coq.Reals.RIneq]
Rmult_le_ge_compat_neg_l [lemma, in Coq.Reals.RIneq]
Rmult_le_pos [lemma, in Coq.Reals.RIneq]
Rmult_le_reg_l [lemma, in Coq.Reals.RIneq]
Rmult_le_0_lt_compat [lemma, in Coq.Reals.RIneq]
Rmult_lt_compat_l [axiom, in Coq.Reals.Raxioms]
Rmult_lt_compat_r [lemma, in Coq.Reals.RIneq]
Rmult_lt_gt_compat_neg_l [lemma, in Coq.Reals.RIneq]
Rmult_lt_reg_l [lemma, in Coq.Reals.RIneq]
Rmult_lt_0_compat [lemma, in Coq.Reals.RIneq]
Rmult_minus_distr_l [lemma, in Coq.Reals.RIneq]
Rmult_ne [lemma, in Coq.Reals.RIneq]
Rmult_neq_0_reg [lemma, in Coq.Reals.RIneq]
Rmult_opp_opp [lemma, in Coq.Reals.RIneq]
Rmult_plus_distr_l [axiom, in Coq.Reals.Raxioms]
Rmult_plus_distr_r [lemma, in Coq.Reals.RIneq]
Rmult_0_l [lemma, in Coq.Reals.RIneq]
Rmult_0_r [lemma, in Coq.Reals.RIneq]
Rmult_1_l [axiom, in Coq.Reals.Raxioms]
Rmult_1_r [lemma, in Coq.Reals.RIneq]
Rnot_ge_gt [lemma, in Coq.Reals.RIneq]
Rnot_ge_lt [lemma, in Coq.Reals.RIneq]
Rnot_gt_ge [lemma, in Coq.Reals.RIneq]
Rnot_gt_le [lemma, in Coq.Reals.RIneq]
Rnot_le_gt [lemma, in Coq.Reals.RIneq]
Rnot_le_lt [lemma, in Coq.Reals.RIneq]
Rnot_lt_ge [lemma, in Coq.Reals.RIneq]
Rnot_lt_le [lemma, in Coq.Reals.RIneq]
RoF [definition, in Coq.Wellfounded.Inverse_Image]
Rof [definition, in Coq.Wellfounded.Inverse_Image]
Rolle [lemma, in Coq.Reals.MVT]
Ropp [axiom, in Coq.Reals.Rdefinitions]
Ropp_eq_compat [lemma, in Coq.Reals.RIneq]
Ropp_eq_0_compat [lemma, in Coq.Reals.RIneq]
Ropp_ge_cancel [lemma, in Coq.Reals.RIneq]
Ropp_ge_contravar [lemma, in Coq.Reals.RIneq]
Ropp_ge_le_contravar [lemma, in Coq.Reals.RIneq]
Ropp_gt_cancel [lemma, in Coq.Reals.RIneq]
Ropp_gt_contravar [lemma, in Coq.Reals.RIneq]
Ropp_gt_lt_contravar [lemma, in Coq.Reals.RIneq]
Ropp_gt_lt_0_contravar [lemma, in Coq.Reals.RIneq]
Ropp_involutive [lemma, in Coq.Reals.RIneq]
Ropp_inv_permute [lemma, in Coq.Reals.RIneq]
Ropp_le_cancel [lemma, in Coq.Reals.RIneq]
Ropp_le_contravar [lemma, in Coq.Reals.RIneq]
Ropp_le_ge_contravar [lemma, in Coq.Reals.RIneq]
Ropp_lt_cancel [lemma, in Coq.Reals.RIneq]
Ropp_lt_contravar [lemma, in Coq.Reals.RIneq]
Ropp_lt_gt_contravar [lemma, in Coq.Reals.RIneq]
Ropp_lt_gt_0_contravar [lemma, in Coq.Reals.RIneq]
Ropp_minus_distr [lemma, in Coq.Reals.RIneq]
Ropp_minus_distr' [lemma, in Coq.Reals.RIneq]
Ropp_mult_distr_l_reverse [lemma, in Coq.Reals.RIneq]
Ropp_mult_distr_r_reverse [lemma, in Coq.Reals.RIneq]
Ropp_neq_0_compat [lemma, in Coq.Reals.RIneq]
Ropp_plus_distr [lemma, in Coq.Reals.RIneq]
Ropp_Ropp_IZR [lemma, in Coq.Reals.RIneq]
Ropp_0 [lemma, in Coq.Reals.RIneq]
Ropp_0_ge_le_contravar [lemma, in Coq.Reals.RIneq]
Ropp_0_gt_lt_contravar [lemma, in Coq.Reals.RIneq]
Ropp_0_le_ge_contravar [lemma, in Coq.Reals.RIneq]
Ropp_0_lt_gt_contravar [lemma, in Coq.Reals.RIneq]
rotation_PI2 [lemma, in Coq.Reals.Rgeom]
rotation_0 [lemma, in Coq.Reals.Rgeom]
Rplus [inductive, in Coq.Sets.Relations_2]
Rplus [axiom, in Coq.Reals.Rdefinitions]
Rplus_assoc [axiom, in Coq.Reals.Raxioms]
Rplus_comm [axiom, in Coq.Reals.Raxioms]
Rplus_contains_R [lemma, in Coq.Sets.Relations_2_facts]
Rplus_eq_compat_l [lemma, in Coq.Reals.RIneq]
Rplus_eq_reg_l [lemma, in Coq.Reals.RIneq]
Rplus_eq_R0 [lemma, in Coq.Reals.RIneq]
Rplus_eq_0_l [lemma, in Coq.Reals.RIneq]
Rplus_ge_compat [lemma, in Coq.Reals.RIneq]
Rplus_ge_compat_l [lemma, in Coq.Reals.RIneq]
Rplus_ge_compat_r [lemma, in Coq.Reals.RIneq]
Rplus_ge_gt_compat [lemma, in Coq.Reals.RIneq]
Rplus_ge_reg_l [lemma, in Coq.Reals.RIneq]
Rplus_ge_reg_neg_r [lemma, in Coq.Reals.RIneq]
Rplus_gt_compat [lemma, in Coq.Reals.RIneq]
Rplus_gt_compat_l [lemma, in Coq.Reals.RIneq]
Rplus_gt_compat_r [lemma, in Coq.Reals.RIneq]
Rplus_gt_ge_compat [lemma, in Coq.Reals.RIneq]
Rplus_gt_reg_l [lemma, in Coq.Reals.RIneq]
Rplus_gt_reg_neg_r [lemma, in Coq.Reals.RIneq]
Rplus_le_compat [lemma, in Coq.Reals.RIneq]
Rplus_le_compat_l [lemma, in Coq.Reals.RIneq]
Rplus_le_compat_r [lemma, in Coq.Reals.RIneq]
Rplus_le_le_0_compat [lemma, in Coq.Reals.RIneq]
Rplus_le_lt_compat [lemma, in Coq.Reals.RIneq]
Rplus_le_lt_0_compat [lemma, in Coq.Reals.RIneq]
Rplus_le_reg_l [lemma, in Coq.Reals.RIneq]
Rplus_le_reg_pos_r [lemma, in Coq.Reals.RIneq]
Rplus_lt_compat [lemma, in Coq.Reals.RIneq]
Rplus_lt_compat_l [axiom, in Coq.Reals.Raxioms]
Rplus_lt_compat_r [lemma, in Coq.Reals.RIneq]
Rplus_lt_le_compat [lemma, in Coq.Reals.RIneq]
Rplus_lt_le_0_compat [lemma, in Coq.Reals.RIneq]
Rplus_lt_pos [lemma, in Coq.Reals.DiscrR]
Rplus_lt_reg_pos_r [lemma, in Coq.Reals.RIneq]
Rplus_lt_reg_r [lemma, in Coq.Reals.RIneq]
Rplus_lt_0_compat [lemma, in Coq.Reals.RIneq]
Rplus_minus [lemma, in Coq.Reals.RIneq]
Rplus_n [constructor, in Coq.Sets.Relations_2]
Rplus_ne [lemma, in Coq.Reals.RIneq]
Rplus_opp_l [lemma, in Coq.Reals.RIneq]
Rplus_opp_r [axiom, in Coq.Reals.Raxioms]
Rplus_opp_r_uniq [lemma, in Coq.Reals.RIneq]
Rplus_sqr_eq_0 [lemma, in Coq.Reals.RIneq]
Rplus_sqr_eq_0_l [lemma, in Coq.Reals.RIneq]
Rplus_0 [constructor, in Coq.Sets.Relations_2]
Rplus_0_l [axiom, in Coq.Reals.Raxioms]
Rplus_0_r [lemma, in Coq.Reals.RIneq]
Rplus_0_r_uniq [lemma, in Coq.Reals.RIneq]
Rpower [definition, in Coq.Reals.Rpower]
Rpower [library]
Rpower_lt [lemma, in Coq.Reals.Rpower]
Rpower_mult [lemma, in Coq.Reals.Rpower]
Rpower_O [lemma, in Coq.Reals.Rpower]
Rpower_plus [lemma, in Coq.Reals.Rpower]
Rpower_pow [lemma, in Coq.Reals.Rpower]
Rpower_Ropp [lemma, in Coq.Reals.Rpower]
Rpower_sqrt [lemma, in Coq.Reals.Rpower]
Rpower_1 [lemma, in Coq.Reals.Rpower]
RPow_abs [lemma, in Coq.Reals.Rfunctions]
Rpow_def [library]
Rprod [library]
RRle_abs [lemma, in Coq.Reals.Rbasic_fun]
Rsepare [lemma, in Coq.Reals.Rtopology]
Rseries [library]
Rseries_CV_comp [lemma, in Coq.Reals.SeqSeries]
Rsigma [library]
Rsqr [definition, in Coq.Reals.RIneq]
Rsqrt [definition, in Coq.Reals.Rsqrt_def]
Rsqrt_def [library]
Rsqrt_exists [lemma, in Coq.Reals.Rsqrt_def]
Rsqrt_positivity [lemma, in Coq.Reals.Rsqrt_def]
Rsqrt_Rsqrt [lemma, in Coq.Reals.Rsqrt_def]
Rsqr_abs [lemma, in Coq.Reals.R_sqr]
Rsqr_div [lemma, in Coq.Reals.R_sqr]
Rsqr_eq [lemma, in Coq.Reals.R_sqr]
Rsqr_eq_abs_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_eq_asb_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_eq_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_gt_0_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_incrst_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_incrst_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_incr_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_incr_0_var [lemma, in Coq.Reals.R_sqr]
Rsqr_incr_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_inj [lemma, in Coq.Reals.R_sqr]
Rsqr_inv [lemma, in Coq.Reals.R_sqr]
Rsqr_le_abs_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_le_abs_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_lt_abs_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_lt_abs_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_minus [lemma, in Coq.Reals.R_sqr]
Rsqr_minus_plus [lemma, in Coq.Reals.R_sqr]
Rsqr_mult [lemma, in Coq.Reals.R_sqr]
Rsqr_neg [lemma, in Coq.Reals.R_sqr]
Rsqr_neg_minus [lemma, in Coq.Reals.R_sqr]
Rsqr_neg_pos_le_0 [lemma, in Coq.Reals.R_sqr]
Rsqr_neg_pos_le_1 [lemma, in Coq.Reals.R_sqr]
Rsqr_plus [lemma, in Coq.Reals.R_sqr]
Rsqr_plus_minus [lemma, in Coq.Reals.R_sqr]
Rsqr_pos_lt [lemma, in Coq.Reals.R_sqr]
Rsqr_sin_cos_d_one [lemma, in Coq.Reals.Rtrigo_calc]
Rsqr_sol_eq_0_0 [lemma, in Coq.Reals.R_sqrt]
Rsqr_sol_eq_0_1 [lemma, in Coq.Reals.R_sqrt]
Rsqr_sqrt [lemma, in Coq.Reals.R_sqrt]
Rsqr_0 [lemma, in Coq.Reals.RIneq]
Rsqr_0_uniq [lemma, in Coq.Reals.RIneq]
Rsqr_1 [lemma, in Coq.Reals.R_sqr]
Rstar [inductive, in Coq.Sets.Relations_2]
RstarRplus_RRstar [lemma, in Coq.Sets.Relations_2_facts]
Rstar1 [inductive, in Coq.Sets.Relations_2]
Rstar1_n [constructor, in Coq.Sets.Relations_2]
Rstar1_0 [constructor, in Coq.Sets.Relations_2]
Rstar1_1 [constructor, in Coq.Sets.Relations_2]
Rstar_cases [lemma, in Coq.Sets.Relations_2_facts]
Rstar_contains_R [lemma, in Coq.Sets.Relations_2_facts]
Rstar_contains_Rplus [lemma, in Coq.Sets.Relations_2_facts]
Rstar_equiv_Rstar1 [lemma, in Coq.Sets.Relations_2_facts]
Rstar_imp_coherent [lemma, in Coq.Sets.Relations_3_facts]
Rstar_n [constructor, in Coq.Sets.Relations_2]
Rstar_reflexive [lemma, in Coq.Sets.Relations_2_facts]
Rstar_transitive [lemma, in Coq.Sets.Relations_2_facts]
Rstar_0 [constructor, in Coq.Sets.Relations_2]
rst_refl [constructor, in Coq.Relations.Relation_Operators]
rst_step [constructor, in Coq.Relations.Relation_Operators]
rst_sym [constructor, in Coq.Relations.Relation_Operators]
rst_trans [constructor, in Coq.Relations.Relation_Operators]
Rsum_abs [lemma, in Coq.Reals.PartSum]
Rsym_imp_notRsym [lemma, in Coq.Sets.Relations_1_facts]
Rsym_imp_Rstarsym [lemma, in Coq.Sets.Relations_2_facts]
Rtail [definition, in Coq.Reals.RList]
rtn1_refl [constructor, in Coq.Relations.Relation_Operators]
rtn1_trans [lemma, in Coq.Relations.Operators_Properties]
rtn1_trans [constructor, in Coq.Relations.Relation_Operators]
rtn1_trans_equiv [lemma, in Coq.Relations.Operators_Properties]
Rtopology [library]
Rtotal_order [lemma, in Coq.Reals.RIneq]
Rtrigo [library]
Rtrigo_alt [library]
Rtrigo_calc [library]
Rtrigo_def [library]
Rtrigo_fun [library]
Rtrigo_reg [library]
rtsn1_refl [constructor, in Coq.Relations.Relation_Operators]
rtsn1_rts [lemma, in Coq.Relations.Operators_Properties]
rtsn1_sym [lemma, in Coq.Relations.Operators_Properties]
rtsn1_trans [lemma, in Coq.Relations.Operators_Properties]
rtsn1_trans [constructor, in Coq.Relations.Relation_Operators]
rts1n_refl [constructor, in Coq.Relations.Relation_Operators]
rts1n_rts [lemma, in Coq.Relations.Operators_Properties]
rts1n_sym [lemma, in Coq.Relations.Operators_Properties]
rts1n_trans [constructor, in Coq.Relations.Relation_Operators]
rts_rtsn1 [lemma, in Coq.Relations.Operators_Properties]
rts_rtsn1_equiv [lemma, in Coq.Relations.Operators_Properties]
rts_rts1n [lemma, in Coq.Relations.Operators_Properties]
rts_rts1n_equiv [lemma, in Coq.Relations.Operators_Properties]
rts_1n_trans [lemma, in Coq.Relations.Operators_Properties]
rt1n_ind_right [lemma, in Coq.Relations.Operators_Properties]
rt1n_refl [constructor, in Coq.Relations.Relation_Operators]
rt1n_trans [lemma, in Coq.Relations.Operators_Properties]
rt1n_trans [constructor, in Coq.Relations.Relation_Operators]
rt1n_trans_equiv [lemma, in Coq.Relations.Operators_Properties]
rt_refl [constructor, in Coq.Relations.Relation_Operators]
rt_step [constructor, in Coq.Relations.Relation_Operators]
rt_trans [constructor, in Coq.Relations.Relation_Operators]
R0 [axiom, in Coq.Reals.Rdefinitions]
R0_fp_O [lemma, in Coq.Reals.R_Ifp]
R1 [axiom, in Coq.Reals.Rdefinitions]
R1_neq_R0 [axiom, in Coq.Reals.Raxioms]
R1_sqrt2_neq_0 [lemma, in Coq.Reals.Rtrigo_calc]
R_complete [lemma, in Coq.Reals.Rcomplete]
R_dist [definition, in Coq.Reals.Rfunctions]
R_dist_eq [lemma, in Coq.Reals.Rfunctions]
R_dist_plus [lemma, in Coq.Reals.Rfunctions]
R_dist_pos [lemma, in Coq.Reals.Rfunctions]
R_dist_refl [lemma, in Coq.Reals.Rfunctions]
R_dist_sym [lemma, in Coq.Reals.Rfunctions]
R_dist_tri [lemma, in Coq.Reals.Rfunctions]
R_Ifp [library]
R_met [definition, in Coq.Reals.Rlimit]
R_rtn1 [lemma, in Coq.Relations.Operators_Properties]
R_rt1n [lemma, in Coq.Relations.Operators_Properties]
R_sqr [library]
R_sqrt [library]
R_wf [definition, in Coq.ZArith.Wf_Z]



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 _ (13564 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 _ (95 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 _ (211 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 _ (71 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 _ (6947 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 _ (305 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 _ (352 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 _ (295 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 _ (183 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 _ (2870 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 _ (287 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 _ (433 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 _ (1189 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 _ (326 entries)