| 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 | (21801 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 | (910 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 | (729 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |
R (lemma)
Rabs_triang_gen [in Coq.Reals.PartSum]Rabs_4 [in Coq.Reals.Ranalysis2]
Rabs_Zabs [in Coq.Reals.Rbasic_fun]
Rabs_def2 [in Coq.Reals.Rbasic_fun]
Rabs_def1 [in Coq.Reals.Rbasic_fun]
Rabs_triang_inv2 [in Coq.Reals.Rbasic_fun]
Rabs_triang_inv [in Coq.Reals.Rbasic_fun]
Rabs_triang [in Coq.Reals.Rbasic_fun]
Rabs_Ropp [in Coq.Reals.Rbasic_fun]
Rabs_Rinv [in Coq.Reals.Rbasic_fun]
Rabs_mult [in Coq.Reals.Rbasic_fun]
Rabs_minus_sym [in Coq.Reals.Rbasic_fun]
Rabs_pos_lt [in Coq.Reals.Rbasic_fun]
Rabs_Rabsolu [in Coq.Reals.Rbasic_fun]
Rabs_pos_eq [in Coq.Reals.Rbasic_fun]
Rabs_le [in Coq.Reals.Rbasic_fun]
Rabs_pos [in Coq.Reals.Rbasic_fun]
Rabs_left1 [in Coq.Reals.Rbasic_fun]
Rabs_right [in Coq.Reals.Rbasic_fun]
Rabs_left [in Coq.Reals.Rbasic_fun]
Rabs_no_R0 [in Coq.Reals.Rbasic_fun]
Rabs_R1 [in Coq.Reals.Rbasic_fun]
Rabs_R0 [in Coq.Reals.Rbasic_fun]
Rabs_derive_2 [in Coq.Reals.Ranalysis4]
Rabs_derive_1 [in Coq.Reals.Ranalysis4]
rad_deg [in Coq.Reals.Rtrigo_calc]
Ratan_is_ps_atan [in Coq.Reals.Ratan]
Ratan_CVU [in Coq.Reals.Ratan]
Ratan_CVU' [in Coq.Reals.Ratan]
Ratan_seq_opp [in Coq.Reals.Ratan]
Ratan_seq_converging [in Coq.Reals.Ratan]
Ratan_seq_decreasing [in Coq.Reals.Ratan]
Raw.add_sorted [in Coq.FSets.FMapList]
Raw.add_Inf [in Coq.FSets.FMapList]
Raw.add_3 [in Coq.FSets.FMapList]
Raw.add_2 [in Coq.FSets.FMapList]
Raw.add_1 [in Coq.FSets.FMapList]
Raw.add_not_eq [in Coq.FSets.FMapWeakList]
Raw.add_eq [in Coq.FSets.FMapWeakList]
Raw.add_NoDup [in Coq.FSets.FMapWeakList]
Raw.add_3' [in Coq.FSets.FMapWeakList]
Raw.add_3 [in Coq.FSets.FMapWeakList]
Raw.add_2 [in Coq.FSets.FMapWeakList]
Raw.add_1 [in Coq.FSets.FMapWeakList]
Raw.combine_1 [in Coq.FSets.FMapList]
Raw.combine_sorted [in Coq.FSets.FMapList]
Raw.combine_lelistA [in Coq.FSets.FMapList]
Raw.combine_1 [in Coq.FSets.FMapWeakList]
Raw.combine_r_1 [in Coq.FSets.FMapWeakList]
Raw.combine_l_1 [in Coq.FSets.FMapWeakList]
Raw.combine_NoDup [in Coq.FSets.FMapWeakList]
Raw.elements_3w [in Coq.FSets.FMapList]
Raw.elements_3 [in Coq.FSets.FMapList]
Raw.elements_2 [in Coq.FSets.FMapList]
Raw.elements_1 [in Coq.FSets.FMapList]
Raw.elements_3w [in Coq.FSets.FMapWeakList]
Raw.elements_2 [in Coq.FSets.FMapWeakList]
Raw.elements_1 [in Coq.FSets.FMapWeakList]
Raw.empty_sorted [in Coq.FSets.FMapList]
Raw.empty_1 [in Coq.FSets.FMapList]
Raw.empty_NoDup [in Coq.FSets.FMapWeakList]
Raw.empty_1 [in Coq.FSets.FMapWeakList]
Raw.equal_cons [in Coq.FSets.FMapList]
Raw.equal_2 [in Coq.FSets.FMapList]
Raw.equal_1 [in Coq.FSets.FMapList]
Raw.equal_2 [in Coq.FSets.FMapWeakList]
Raw.equal_1 [in Coq.FSets.FMapWeakList]
Raw.find_1 [in Coq.FSets.FMapList]
Raw.find_2 [in Coq.FSets.FMapList]
Raw.find_eq [in Coq.FSets.FMapWeakList]
Raw.find_1 [in Coq.FSets.FMapWeakList]
Raw.find_2 [in Coq.FSets.FMapWeakList]
Raw.fold_1 [in Coq.FSets.FMapList]
Raw.fold_right_pair_NoDup [in Coq.FSets.FMapWeakList]
Raw.fold_1 [in Coq.FSets.FMapWeakList]
Raw.is_empty_2 [in Coq.FSets.FMapList]
Raw.is_empty_1 [in Coq.FSets.FMapList]
Raw.is_empty_2 [in Coq.FSets.FMapWeakList]
Raw.is_empty_1 [in Coq.FSets.FMapWeakList]
Raw.mapi_sorted [in Coq.FSets.FMapList]
Raw.mapi_lelistA [in Coq.FSets.FMapList]
Raw.mapi_2 [in Coq.FSets.FMapList]
Raw.mapi_1 [in Coq.FSets.FMapList]
Raw.mapi_NoDup [in Coq.FSets.FMapWeakList]
Raw.mapi_2 [in Coq.FSets.FMapWeakList]
Raw.mapi_1 [in Coq.FSets.FMapWeakList]
Raw.map_sorted [in Coq.FSets.FMapList]
Raw.map_lelistA [in Coq.FSets.FMapList]
Raw.map_2 [in Coq.FSets.FMapList]
Raw.map_1 [in Coq.FSets.FMapList]
Raw.map_NoDup [in Coq.FSets.FMapWeakList]
Raw.map_2 [in Coq.FSets.FMapWeakList]
Raw.map_1 [in Coq.FSets.FMapWeakList]
Raw.map2_2 [in Coq.FSets.FMapList]
Raw.map2_1 [in Coq.FSets.FMapList]
Raw.map2_0 [in Coq.FSets.FMapList]
Raw.map2_sorted [in Coq.FSets.FMapList]
Raw.map2_alt_equiv [in Coq.FSets.FMapList]
Raw.map2_2 [in Coq.FSets.FMapWeakList]
Raw.map2_1 [in Coq.FSets.FMapWeakList]
Raw.map2_0 [in Coq.FSets.FMapWeakList]
Raw.map2_NoDup [in Coq.FSets.FMapWeakList]
Raw.mem_2 [in Coq.FSets.FMapList]
Raw.mem_1 [in Coq.FSets.FMapList]
Raw.mem_2 [in Coq.FSets.FMapWeakList]
Raw.mem_1 [in Coq.FSets.FMapWeakList]
Raw.Proofs.add_find [in Coq.FSets.FMapAVL]
Raw.Proofs.add_3 [in Coq.FSets.FMapAVL]
Raw.Proofs.add_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.add_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.add_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.add_in [in Coq.FSets.FMapAVL]
Raw.Proofs.bal_find [in Coq.FSets.FMapAVL]
Raw.Proofs.bal_mapsto [in Coq.FSets.FMapAVL]
Raw.Proofs.bal_in [in Coq.FSets.FMapAVL]
Raw.Proofs.bal_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.concat_find [in Coq.FSets.FMapAVL]
Raw.Proofs.concat_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.concat_in [in Coq.FSets.FMapAVL]
Raw.Proofs.cons_IfEq [in Coq.FSets.FMapAVL]
Raw.Proofs.cons_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.create_in [in Coq.FSets.FMapAVL]
Raw.Proofs.create_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_node [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_app [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_cardinal [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_cardinal [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_nodup [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_sort [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_sort [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_in [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_mapsto [in Coq.FSets.FMapAVL]
Raw.Proofs.elements_aux_mapsto [in Coq.FSets.FMapAVL]
Raw.Proofs.empty_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.empty_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.equal_Equivb [in Coq.FSets.FMapAVL]
Raw.Proofs.equal_IfEq [in Coq.FSets.FMapAVL]
Raw.Proofs.equal_cont_IfEq [in Coq.FSets.FMapAVL]
Raw.Proofs.equal_more_IfEq [in Coq.FSets.FMapAVL]
Raw.Proofs.equal_end_IfEq [in Coq.FSets.FMapAVL]
Raw.Proofs.Equivb_elements [in Coq.FSets.FMapAVL]
Raw.Proofs.find_in_equiv [in Coq.FSets.FMapAVL]
Raw.Proofs.find_mapsto_equiv [in Coq.FSets.FMapAVL]
Raw.Proofs.find_find [in Coq.FSets.FMapAVL]
Raw.Proofs.find_in_iff [in Coq.FSets.FMapAVL]
Raw.Proofs.find_in [in Coq.FSets.FMapAVL]
Raw.Proofs.find_iff [in Coq.FSets.FMapAVL]
Raw.Proofs.find_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.find_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e_elements [in Coq.FSets.FMapAVL]
Raw.Proofs.fold_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.fold_equiv [in Coq.FSets.FMapAVL]
Raw.Proofs.fold_equiv_aux [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_trans [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_not_in [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_right [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_left [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_tree_node [in Coq.FSets.FMapAVL]
Raw.Proofs.gt_leaf [in Coq.FSets.FMapAVL]
Raw.Proofs.in_find [in Coq.FSets.FMapAVL]
Raw.Proofs.In_node_iff [in Coq.FSets.FMapAVL]
Raw.Proofs.In_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.In_alt [in Coq.FSets.FMapAVL]
Raw.Proofs.In_MapsTo [in Coq.FSets.FMapAVL]
Raw.Proofs.is_empty_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.is_empty_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.join_find [in Coq.FSets.FMapAVL]
Raw.Proofs.join_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.join_in [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_tree_trans [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_tree_not_in [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_right [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_left [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_tree_node [in Coq.FSets.FMapAVL]
Raw.Proofs.lt_leaf [in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.mapi_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.MapsTo_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.MapsTo_In [in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_find [in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.map_option_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.map_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.map_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.map_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.mem_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.mem_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.merge_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.merge_mapsto [in Coq.FSets.FMapAVL]
Raw.Proofs.merge_in [in Coq.FSets.FMapAVL]
Raw.Proofs.not_find_iff [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_3 [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_1 [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_in [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_find [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_gt_tree [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_mapsto [in Coq.FSets.FMapAVL]
Raw.Proofs.remove_min_in [in Coq.FSets.FMapAVL]
Raw.Proofs.split_find [in Coq.FSets.FMapAVL]
Raw.Proofs.split_gt_tree [in Coq.FSets.FMapAVL]
Raw.Proofs.split_lt_tree [in Coq.FSets.FMapAVL]
Raw.Proofs.split_bst [in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_3 [in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_2 [in Coq.FSets.FMapAVL]
Raw.Proofs.split_in_1 [in Coq.FSets.FMapAVL]
Raw.remove_sorted [in Coq.FSets.FMapList]
Raw.remove_Inf [in Coq.FSets.FMapList]
Raw.remove_3 [in Coq.FSets.FMapList]
Raw.remove_2 [in Coq.FSets.FMapList]
Raw.remove_1 [in Coq.FSets.FMapList]
Raw.remove_NoDup [in Coq.FSets.FMapWeakList]
Raw.remove_3' [in Coq.FSets.FMapWeakList]
Raw.remove_3 [in Coq.FSets.FMapWeakList]
Raw.remove_2 [in Coq.FSets.FMapWeakList]
Raw.remove_1 [in Coq.FSets.FMapWeakList]
Raw.submap_2 [in Coq.FSets.FMapWeakList]
Raw.submap_1 [in Coq.FSets.FMapWeakList]
Raw2SetsOn.choose_spec3 [in Coq.MSets.MSetInterface]
Raw2SetsOn.compare_spec [in Coq.MSets.MSetInterface]
Raw2SetsOn.elements_spec2 [in Coq.MSets.MSetInterface]
Raw2SetsOn.max_elt_spec3 [in Coq.MSets.MSetInterface]
Raw2SetsOn.max_elt_spec2 [in Coq.MSets.MSetInterface]
Raw2SetsOn.max_elt_spec1 [in Coq.MSets.MSetInterface]
Raw2SetsOn.min_elt_spec3 [in Coq.MSets.MSetInterface]
Raw2SetsOn.min_elt_spec2 [in Coq.MSets.MSetInterface]
Raw2SetsOn.min_elt_spec1 [in Coq.MSets.MSetInterface]
Rcase_abs [in Coq.Reals.Rbasic_fun]
Rcompare_spec [in Coq.Reals.ROrderedType]
Rcontinuity_abs [in Coq.Reals.Ranalysis4]
Rdef_pow_add [in Coq.setoid_ring.RealField]
Rderivable_pt_abs [in Coq.Reals.Ranalysis4]
Rdichotomy [in Coq.Reals.RIneq]
Rdiv_minus_distr [in Coq.Reals.RIneq]
Rdiv_plus_distr [in Coq.Reals.RIneq]
Rdiv_lt_0_compat [in Coq.Reals.RIneq]
rdiv_r_r [in Coq.setoid_ring.Field_theory]
rdiv_simpl [in Coq.setoid_ring.Field_theory]
rdiv1 [in Coq.setoid_ring.Field_theory]
rdiv2 [in Coq.setoid_ring.Field_theory]
rdiv2b [in Coq.setoid_ring.Field_theory]
rdiv3b [in Coq.setoid_ring.Field_theory]
rdiv4 [in Coq.setoid_ring.Field_theory]
rdiv4b [in Coq.setoid_ring.Field_theory]
rdiv5 [in Coq.setoid_ring.Field_theory]
rdiv6 [in Coq.setoid_ring.Field_theory]
rdiv7 [in Coq.setoid_ring.Field_theory]
rdiv7b [in Coq.setoid_ring.Field_theory]
rdiv8 [in Coq.setoid_ring.Field_theory]
recrbis_equiv [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recrbis_aux_equiv [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_eqn [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_aux_converges [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_aux_eqn [in Coq.Numbers.Cyclic.Int31.Cyclic31]
reduce_aux_le_compat [in Coq.btauto.Algebra]
reduce_eval_compat [in Coq.btauto.Algebra]
reduce_aux_eval_compat [in Coq.btauto.Algebra]
reduce_poly_of_formula_sound_alt [in Coq.btauto.Reflect]
reduce_poly_of_formula_sound [in Coq.btauto.Reflect]
Reflect [in Coq.rtauto.Rtauto]
reflect_dec [in Coq.Bool.Bool]
reflect_iff [in Coq.Bool.Bool]
reflexive_proper [in Coq.Classes.Morphisms]
Reflexive_partial_app_morphism [in Coq.Classes.Morphisms]
reflexive_proper_proxy [in Coq.Classes.Morphisms]
reflexive_proper [in Coq.Classes.CMorphisms]
Reflexive_partial_app_morphism [in Coq.Classes.CMorphisms]
reflexive_proper_proxy [in Coq.Classes.CMorphisms]
relative_non_contradiction_of_definite_descr [in Coq.Logic.ChoiceFacts]
relative_non_contradiction_of_indefinite_descr [in Coq.Logic.ChoiceFacts]
rel_choice_indep_of_general_premises_imp_guarded_rel_choice [in Coq.Logic.ChoiceFacts]
rel_choice_and_proof_irrel_imp_guarded_rel_choice [in Coq.Logic.ChoiceFacts]
rel_prime_le_prime [in Coq.ZArith.Znumtheory]
rel_prime_mod_rev [in Coq.ZArith.Znumtheory]
rel_prime_mod [in Coq.ZArith.Znumtheory]
rel_prime_1 [in Coq.ZArith.Znumtheory]
rel_prime_div [in Coq.ZArith.Znumtheory]
rel_prime_sym [in Coq.ZArith.Znumtheory]
rel_prime_cross_prod [in Coq.ZArith.Znumtheory]
rel_prime_mult [in Coq.ZArith.Znumtheory]
rel_prime_bezout [in Coq.ZArith.Znumtheory]
rel_prime_Zpower [in Coq.ZArith.Zpow_facts]
rel_prime_Zpower_r [in Coq.ZArith.Zpow_facts]
Remainder_equiv [in Coq.ZArith.Zquot]
Remainder_equiv [in Coq.ZArith.Zdiv]
removeA_equivlistA [in Coq.Lists.SetoidList]
removeA_NoDupA [in Coq.Lists.SetoidList]
removeA_InA [in Coq.Lists.SetoidList]
removeA_filter [in Coq.Lists.SetoidList]
removelast_firstn [in Coq.Lists.List]
removelast_app [in Coq.Lists.List]
remove_In [in Coq.Lists.List]
repeat_spec [in Coq.Lists.List]
repeat_length [in Coq.Lists.List]
representative_boolean_partition_imp_excluded_middle [in Coq.Logic.ClassicalFacts]
representative_choice [in Coq.Logic.SetoidChoice]
repr_fun_choice_imp_relational_choice [in Coq.Logic.ChoiceFacts]
repr_fun_choice_imp_excluded_middle [in Coq.Logic.ChoiceFacts]
repr_fun_choice_imp_ext_function_repr [in Coq.Logic.ChoiceFacts]
repr_fun_choice_imp_ext_pred_repr [in Coq.Logic.ChoiceFacts]
repr_fun_choice_imp_ext_prop_repr [in Coq.Logic.ChoiceFacts]
Reqb_eq [in Coq.Reals.ROrderedType]
Req_EM_T [in Coq.Reals.RIneq]
Req_ge_sym [in Coq.Reals.RIneq]
Req_le_sym [in Coq.Reals.RIneq]
Req_ge [in Coq.Reals.RIneq]
Req_le [in Coq.Reals.RIneq]
Req_dec [in Coq.Reals.RIneq]
req_trans [in Coq.micromega.ZCoeff]
req_sym [in Coq.micromega.ZCoeff]
req_refl [in Coq.micromega.ZCoeff]
Req_dne [in Coq.micromega.OrderedRing]
Req_em [in Coq.micromega.OrderedRing]
Req_dec [in Coq.Reals.ROrderedType]
Reste_E_cv [in Coq.Reals.Exp_prop]
Reste_E_maj [in Coq.Reals.Exp_prop]
reste_cv_R0 [in Coq.Reals.Cos_plus]
reste1_cv_R0 [in Coq.Reals.Cos_plus]
reste1_maj [in Coq.Reals.Cos_plus]
reste2_cv_R0 [in Coq.Reals.Cos_plus]
reste2_maj [in Coq.Reals.Cos_plus]
restriction_family [in Coq.Reals.Rtopology]
retract_pow_U_U [in Coq.Logic.Berardi]
Reval_nformula_dec [in Coq.micromega.RMicromega]
Reval_formula_compat [in Coq.micromega.RMicromega]
revapp_nil_inv [in Coq.Numbers.DecimalFacts]
rev_trans [in Coq.ssr.ssrbool]
rev_lnorm_rev [in Coq.Numbers.DecimalFacts]
rev_nil_inv [in Coq.Numbers.DecimalFacts]
rev_nztail_rev [in Coq.Numbers.DecimalFacts]
rev_rev [in Coq.Numbers.DecimalFacts]
rev_revapp [in Coq.Numbers.DecimalFacts]
rev_ind [in Coq.Lists.List]
rev_list_ind [in Coq.Lists.List]
rev_alt [in Coq.Lists.List]
rev_append_rev [in Coq.Lists.List]
rev_nth [in Coq.Lists.List]
rev_length [in Coq.Lists.List]
rev_involutive [in Coq.Lists.List]
rev_unit [in Coq.Lists.List]
rev_app_distr [in Coq.Lists.List]
rew_ex2 [in Coq.Init.Logic]
rew_ex [in Coq.Init.Logic]
rew_const [in Coq.Init.Logic]
rew_opp_l [in Coq.Init.Logic]
rew_opp_r [in Coq.Init.Logic]
rew_sig2 [in Coq.Init.Specif]
rew_sigT2 [in Coq.Init.Specif]
rew_sig [in Coq.Init.Specif]
rew_sigT [in Coq.Init.Specif]
Rext [in Coq.nsatz.Nsatz]
RfactN_fact2N_factk [in Coq.Reals.Rprod]
Rfield [in Coq.setoid_ring.RealField]
Rgen_phiPOS_not_0 [in Coq.setoid_ring.RealField]
Rgen_phiPOS [in Coq.setoid_ring.RealField]
Rge_minus [in Coq.Reals.RIneq]
Rge_or_gt [in Coq.Reals.RIneq]
Rge_gt_dec [in Coq.Reals.RIneq]
Rge_dec [in Coq.Reals.RIneq]
Rge_gt_trans [in Coq.Reals.RIneq]
Rge_trans [in Coq.Reals.RIneq]
Rge_ge_eq [in Coq.Reals.RIneq]
Rge_antisym [in Coq.Reals.RIneq]
Rge_not_gt [in Coq.Reals.RIneq]
Rge_not_lt [in Coq.Reals.RIneq]
Rge_le [in Coq.Reals.RIneq]
Rge_refl [in Coq.Reals.RIneq]
Rgt_minus [in Coq.Reals.RIneq]
Rgt_or_ge [in Coq.Reals.RIneq]
Rgt_ge_dec [in Coq.Reals.RIneq]
Rgt_dec [in Coq.Reals.RIneq]
Rgt_ge_trans [in Coq.Reals.RIneq]
Rgt_trans [in Coq.Reals.RIneq]
Rgt_eq_compat [in Coq.Reals.RIneq]
Rgt_asym [in Coq.Reals.RIneq]
Rgt_not_ge [in Coq.Reals.RIneq]
Rgt_not_le [in Coq.Reals.RIneq]
Rgt_lt [in Coq.Reals.RIneq]
Rgt_ge [in Coq.Reals.RIneq]
Rgt_not_eq [in Coq.Reals.RIneq]
Rgt_irrefl [in Coq.Reals.RIneq]
Rgt_2PI_0 [in Coq.Reals.Rtrigo_calc]
Rgt_3PI2_0 [in Coq.Reals.Rtrigo_calc]
RiemannInt_const_bound [in Coq.Reals.RiemannInt]
RiemannInt_P33 [in Coq.Reals.RiemannInt]
RiemannInt_P32 [in Coq.Reals.RiemannInt]
RiemannInt_P31 [in Coq.Reals.RiemannInt]
RiemannInt_P30 [in Coq.Reals.RiemannInt]
RiemannInt_P29 [in Coq.Reals.RiemannInt]
RiemannInt_P28 [in Coq.Reals.RiemannInt]
RiemannInt_P27 [in Coq.Reals.RiemannInt]
RiemannInt_P26 [in Coq.Reals.RiemannInt]
RiemannInt_P25 [in Coq.Reals.RiemannInt]
RiemannInt_P24 [in Coq.Reals.RiemannInt]
RiemannInt_P23 [in Coq.Reals.RiemannInt]
RiemannInt_P22 [in Coq.Reals.RiemannInt]
RiemannInt_P21 [in Coq.Reals.RiemannInt]
RiemannInt_P20 [in Coq.Reals.RiemannInt]
RiemannInt_P19 [in Coq.Reals.RiemannInt]
RiemannInt_P18 [in Coq.Reals.RiemannInt]
RiemannInt_P17 [in Coq.Reals.RiemannInt]
RiemannInt_P16 [in Coq.Reals.RiemannInt]
RiemannInt_P15 [in Coq.Reals.RiemannInt]
RiemannInt_P14 [in Coq.Reals.RiemannInt]
RiemannInt_P13 [in Coq.Reals.RiemannInt]
RiemannInt_P12 [in Coq.Reals.RiemannInt]
RiemannInt_P11 [in Coq.Reals.RiemannInt]
RiemannInt_P10 [in Coq.Reals.RiemannInt]
RiemannInt_P9 [in Coq.Reals.RiemannInt]
RiemannInt_P8 [in Coq.Reals.RiemannInt]
RiemannInt_P7 [in Coq.Reals.RiemannInt]
RiemannInt_P6 [in Coq.Reals.RiemannInt]
RiemannInt_P5 [in Coq.Reals.RiemannInt]
RiemannInt_P4 [in Coq.Reals.RiemannInt]
RiemannInt_exists [in Coq.Reals.RiemannInt]
RiemannInt_P3 [in Coq.Reals.RiemannInt]
RiemannInt_P2 [in Coq.Reals.RiemannInt]
RiemannInt_P1 [in Coq.Reals.RiemannInt]
Riemann_integrable_Ropp [in Coq.Reals.RiemannInt]
Riemann_integrable_scal [in Coq.Reals.RiemannInt]
Riemann_integrable_ext [in Coq.Reals.RiemannInt]
right_prefix [in Coq.Wellfounded.Lexicographic_Exponentiation]
ring_S_inj [in Coq.setoid_ring.Field_theory]
ring_opp_zero [in Coq.setoid_ring.Ncring]
ring_add_assoc2 [in Coq.setoid_ring.Ncring]
ring_add_assoc1 [in Coq.setoid_ring.Ncring]
ring_add_0_r [in Coq.setoid_ring.Ncring]
ring_sub_ext [in Coq.setoid_ring.Ncring]
ring_opp_opp [in Coq.setoid_ring.Ncring]
ring_opp_add [in Coq.setoid_ring.Ncring]
ring_opp_mul_r [in Coq.setoid_ring.Ncring]
ring_opp_mul_l [in Coq.setoid_ring.Ncring]
ring_mul_0_r [in Coq.setoid_ring.Ncring]
ring_mul_0_l [in Coq.setoid_ring.Ncring]
ring_correct [in Coq.setoid_ring.Ncring_polynom]
ring_ops_wd [in Coq.micromega.ZCoeff]
ring_rw_correct [in Coq.setoid_ring.Ring_polynom]
ring_rw_pow_correct [in Coq.setoid_ring.Ring_polynom]
ring_correct [in Coq.setoid_ring.Ring_polynom]
ring_theory_switch_eq [in Coq.Numbers.Cyclic.Int31.Ring31]
Rintegral_domain_pow [in Coq.setoid_ring.Integral_domain]
RinvN_cv [in Coq.Reals.RiemannInt]
RinvN_pos [in Coq.Reals.RiemannInt]
Rinv_le_contravar [in Coq.Reals.RIneq]
Rinv_1_lt_contravar [in Coq.Reals.RIneq]
Rinv_lt_contravar [in Coq.Reals.RIneq]
Rinv_lt_0_compat [in Coq.Reals.RIneq]
Rinv_0_lt_compat [in Coq.Reals.RIneq]
Rinv_mult_simpl [in Coq.Reals.RIneq]
Rinv_r_simpl_m [in Coq.Reals.RIneq]
Rinv_r_simpl_l [in Coq.Reals.RIneq]
Rinv_r_simpl_r [in Coq.Reals.RIneq]
Rinv_mult_distr [in Coq.Reals.RIneq]
Rinv_involutive [in Coq.Reals.RIneq]
Rinv_neq_0_compat [in Coq.Reals.RIneq]
Rinv_1 [in Coq.Reals.RIneq]
Rinv_r_sym [in Coq.Reals.RIneq]
Rinv_l_sym [in Coq.Reals.RIneq]
Rinv_r [in Coq.Reals.RIneq]
Rinv_1 [in Coq.micromega.RMicromega]
rinv_nz [in Coq.setoid_ring.Field_theory]
Rinv_pow [in Coq.Reals.Rfunctions]
Rinv_Rdiv [in Coq.Reals.Rpower]
Rle_Rinv [in Coq.Reals.RIneq]
Rle_lt_0_plus_1 [in Coq.Reals.RIneq]
Rle_0_1 [in Coq.Reals.RIneq]
Rle_0_sqr [in Coq.Reals.RIneq]
Rle_minus [in Coq.Reals.RIneq]
Rle_lt_or_eq_dec [in Coq.Reals.RIneq]
Rle_or_lt [in Coq.Reals.RIneq]
Rle_lt_dec [in Coq.Reals.RIneq]
Rle_dec [in Coq.Reals.RIneq]
Rle_lt_trans [in Coq.Reals.RIneq]
Rle_trans [in Coq.Reals.RIneq]
Rle_le_eq [in Coq.Reals.RIneq]
Rle_antisym [in Coq.Reals.RIneq]
Rle_not_gt [in Coq.Reals.RIneq]
Rle_not_lt [in Coq.Reals.RIneq]
Rle_ge [in Coq.Reals.RIneq]
Rle_refl [in Coq.Reals.RIneq]
Rle_cv_lim [in Coq.Reals.RiemannInt]
Rle_abs [in Coq.Reals.Rbasic_fun]
Rle_max_compat_l [in Coq.Reals.Rbasic_fun]
Rle_max_compat_r [in Coq.Reals.Rbasic_fun]
Rle_min_compat_l [in Coq.Reals.Rbasic_fun]
Rle_min_compat_r [in Coq.Reals.Rbasic_fun]
Rle_Qle [in Coq.QArith.Qreals]
Rle_mult_inv_pos [in Coq.micromega.Fourier_util]
Rle_zero_pos_plus1 [in Coq.micromega.Fourier_util]
Rle_pow [in Coq.Reals.Rfunctions]
Rle_Rpower_l [in Coq.Reals.Rpower]
Rle_Rpower [in Coq.Reals.Rpower]
Rle_le_minus [in Coq.micromega.OrderedRing]
Rle_ngt [in Coq.micromega.OrderedRing]
Rle_gt_cases [in Coq.micromega.OrderedRing]
Rle_lt_trans [in Coq.micromega.OrderedRing]
Rle_lt_eq [in Coq.micromega.OrderedRing]
Rle_trans [in Coq.micromega.OrderedRing]
Rle_antisymm [in Coq.micromega.OrderedRing]
Rle_refl [in Coq.micromega.OrderedRing]
Rle_mult_inv_pos [in Coq.Reals.R_sqrt]
RList_P29 [in Coq.Reals.RList]
RList_P28 [in Coq.Reals.RList]
RList_P27 [in Coq.Reals.RList]
RList_P26 [in Coq.Reals.RList]
RList_P25 [in Coq.Reals.RList]
RList_P24 [in Coq.Reals.RList]
RList_P23 [in Coq.Reals.RList]
RList_P22 [in Coq.Reals.RList]
RList_P21 [in Coq.Reals.RList]
RList_P20 [in Coq.Reals.RList]
RList_P19 [in Coq.Reals.RList]
RList_P18 [in Coq.Reals.RList]
RList_P17 [in Coq.Reals.RList]
RList_P16 [in Coq.Reals.RList]
RList_P15 [in Coq.Reals.RList]
RList_P14 [in Coq.Reals.RList]
RList_P13 [in Coq.Reals.RList]
RList_P12 [in Coq.Reals.RList]
RList_P11 [in Coq.Reals.RList]
RList_P10 [in Coq.Reals.RList]
RList_P9 [in Coq.Reals.RList]
RList_P8 [in Coq.Reals.RList]
RList_P7 [in Coq.Reals.RList]
RList_P6 [in Coq.Reals.RList]
RList_P5 [in Coq.Reals.RList]
RList_P4 [in Coq.Reals.RList]
RList_P3 [in Coq.Reals.RList]
RList_P2 [in Coq.Reals.RList]
RList_P1 [in Coq.Reals.RList]
RList_P0 [in Coq.Reals.RList]
Rlist_P1 [in Coq.Reals.RList]
Rlt_plus_1 [in Coq.Reals.RIneq]
Rlt_0_1 [in Coq.Reals.RIneq]
Rlt_0_sqr [in Coq.Reals.RIneq]
Rlt_Rminus [in Coq.Reals.RIneq]
Rlt_minus [in Coq.Reals.RIneq]
Rlt_or_le [in Coq.Reals.RIneq]
Rlt_le_dec [in Coq.Reals.RIneq]
Rlt_dec [in Coq.Reals.RIneq]
Rlt_le_trans [in Coq.Reals.RIneq]
Rlt_eq_compat [in Coq.Reals.RIneq]
Rlt_not_ge [in Coq.Reals.RIneq]
Rlt_not_le [in Coq.Reals.RIneq]
Rlt_gt [in Coq.Reals.RIneq]
Rlt_le [in Coq.Reals.RIneq]
Rlt_dichotomy_converse [in Coq.Reals.RIneq]
Rlt_not_eq [in Coq.Reals.RIneq]
Rlt_irrefl [in Coq.Reals.RIneq]
Rlt_3PI2_2PI [in Coq.Reals.Rtrigo_calc]
Rlt_PI_3PI2 [in Coq.Reals.Rtrigo_calc]
Rlt_sqrt3_0 [in Coq.Reals.Rtrigo_calc]
Rlt_sqrt2_0 [in Coq.Reals.Rtrigo_calc]
Rlt_0_2 [in Coq.setoid_ring.RealField]
Rlt_n_Sn [in Coq.setoid_ring.RealField]
Rlt_4 [in Coq.Reals.Ranalysis2]
Rlt_Qlt [in Coq.QArith.Qreals]
Rlt_eps4_eps [in Coq.Reals.Rlimit]
Rlt_eps2_eps [in Coq.Reals.Rlimit]
Rlt_zero_pos_plus1 [in Coq.micromega.Fourier_util]
Rlt_mult_inv_pos [in Coq.micromega.Fourier_util]
Rlt_pow [in Coq.Reals.Rfunctions]
Rlt_pow_R1 [in Coq.Reals.Rfunctions]
Rlt_Rpower_l [in Coq.Reals.Rpower]
Rlt_lt_succ [in Coq.micromega.OrderedRing]
Rlt_succ_r [in Coq.micromega.OrderedRing]
Rlt_0_1 [in Coq.micromega.OrderedRing]
Rlt_lt_minus [in Coq.micromega.OrderedRing]
Rlt_nge [in Coq.micromega.OrderedRing]
Rlt_neq [in Coq.micromega.OrderedRing]
Rlt_le_trans [in Coq.micromega.OrderedRing]
Rlt_trans [in Coq.micromega.OrderedRing]
Rlt_le_neq [in Coq.micromega.OrderedRing]
Rlt_trichotomy [in Coq.micromega.OrderedRing]
Rlt_mult_inv_pos [in Coq.Reals.R_sqrt]
Rlt_R0_R2 [in Coq.Reals.DiscrR]
RmaxAbs [in Coq.Reals.Rbasic_fun]
RmaxRmult [in Coq.Reals.Rbasic_fun]
Rmax_r [in Coq.Reals.Rminmax]
Rmax_l [in Coq.Reals.Rminmax]
Rmax_assoc [in Coq.Reals.Rbasic_fun]
Rmax_neg [in Coq.Reals.Rbasic_fun]
Rmax_Rlt [in Coq.Reals.Rbasic_fun]
Rmax_lub_lt [in Coq.Reals.Rbasic_fun]
Rmax_lub [in Coq.Reals.Rbasic_fun]
Rmax_stable_in_negreal [in Coq.Reals.Rbasic_fun]
Rmax_right [in Coq.Reals.Rbasic_fun]
Rmax_left [in Coq.Reals.Rbasic_fun]
Rmax_r [in Coq.Reals.Rbasic_fun]
Rmax_l [in Coq.Reals.Rbasic_fun]
Rmax_comm [in Coq.Reals.Rbasic_fun]
Rmax_Rle [in Coq.Reals.Rbasic_fun]
Rmax_case_strong [in Coq.Reals.Rbasic_fun]
Rmax_case [in Coq.Reals.Rbasic_fun]
Rminmax [in Coq.Reals.Rbasic_fun]
Rminus_ge [in Coq.Reals.RIneq]
Rminus_le [in Coq.Reals.RIneq]
Rminus_gt_0_lt [in Coq.Reals.RIneq]
Rminus_gt [in Coq.Reals.RIneq]
Rminus_lt [in Coq.Reals.RIneq]
Rminus_not_eq_right [in Coq.Reals.RIneq]
Rminus_not_eq [in Coq.Reals.RIneq]
Rminus_eq_contra [in Coq.Reals.RIneq]
Rminus_diag_uniq_sym [in Coq.Reals.RIneq]
Rminus_diag_uniq [in Coq.Reals.RIneq]
Rminus_diag_eq [in Coq.Reals.RIneq]
Rminus_0_l [in Coq.Reals.RIneq]
Rminus_0_r [in Coq.Reals.RIneq]
Rminus_fp2 [in Coq.Reals.R_Ifp]
Rminus_fp1 [in Coq.Reals.R_Ifp]
Rminus_Int_part2 [in Coq.Reals.R_Ifp]
Rminus_Int_part1 [in Coq.Reals.R_Ifp]
Rminus_eq_0 [in Coq.micromega.OrderedRing]
Rmin_r [in Coq.Reals.Rminmax]
Rmin_l [in Coq.Reals.Rminmax]
Rmin_assoc [in Coq.Reals.Rbasic_fun]
Rmin_glb_lt [in Coq.Reals.Rbasic_fun]
Rmin_glb [in Coq.Reals.Rbasic_fun]
Rmin_pos [in Coq.Reals.Rbasic_fun]
Rmin_stable_in_posreal [in Coq.Reals.Rbasic_fun]
Rmin_comm [in Coq.Reals.Rbasic_fun]
Rmin_right [in Coq.Reals.Rbasic_fun]
Rmin_left [in Coq.Reals.Rbasic_fun]
Rmin_r [in Coq.Reals.Rbasic_fun]
Rmin_l [in Coq.Reals.Rbasic_fun]
Rmin_Rgt [in Coq.Reals.Rbasic_fun]
Rmin_Rgt_r [in Coq.Reals.Rbasic_fun]
Rmin_Rgt_l [in Coq.Reals.Rbasic_fun]
Rmin_case_strong [in Coq.Reals.Rbasic_fun]
Rmin_case [in Coq.Reals.Rbasic_fun]
Rmult_ge_0_gt_0_lt_compat [in Coq.Reals.RIneq]
Rmult_le_pos [in Coq.Reals.RIneq]
Rmult_le_reg_r [in Coq.Reals.RIneq]
Rmult_le_reg_l [in Coq.Reals.RIneq]
Rmult_gt_reg_l [in Coq.Reals.RIneq]
Rmult_lt_reg_r [in Coq.Reals.RIneq]
Rmult_lt_reg_l [in Coq.Reals.RIneq]
Rmult_lt_gt_compat_neg_l [in Coq.Reals.RIneq]
Rmult_le_ge_compat_neg_l [in Coq.Reals.RIneq]
Rmult_le_compat_neg_l [in Coq.Reals.RIneq]
Rmult_gt_0_compat [in Coq.Reals.RIneq]
Rmult_lt_0_compat [in Coq.Reals.RIneq]
Rmult_le_0_lt_compat [in Coq.Reals.RIneq]
Rmult_gt_0_lt_compat [in Coq.Reals.RIneq]
Rmult_ge_compat [in Coq.Reals.RIneq]
Rmult_le_compat [in Coq.Reals.RIneq]
Rmult_ge_compat_r [in Coq.Reals.RIneq]
Rmult_ge_compat_l [in Coq.Reals.RIneq]
Rmult_le_compat_r [in Coq.Reals.RIneq]
Rmult_le_compat_l [in Coq.Reals.RIneq]
Rmult_gt_compat_l [in Coq.Reals.RIneq]
Rmult_gt_compat_r [in Coq.Reals.RIneq]
Rmult_lt_compat_r [in Coq.Reals.RIneq]
Rmult_minus_distr_l [in Coq.Reals.RIneq]
Rmult_opp_opp [in Coq.Reals.RIneq]
Rmult_plus_distr_r [in Coq.Reals.RIneq]
Rmult_integral_contrapositive_currified [in Coq.Reals.RIneq]
Rmult_integral_contrapositive [in Coq.Reals.RIneq]
Rmult_neq_0_reg [in Coq.Reals.RIneq]
Rmult_eq_0_compat_l [in Coq.Reals.RIneq]
Rmult_eq_0_compat_r [in Coq.Reals.RIneq]
Rmult_eq_0_compat [in Coq.Reals.RIneq]
Rmult_integral [in Coq.Reals.RIneq]
Rmult_eq_reg_r [in Coq.Reals.RIneq]
Rmult_eq_reg_l [in Coq.Reals.RIneq]
Rmult_eq_compat_r [in Coq.Reals.RIneq]
Rmult_eq_compat_l [in Coq.Reals.RIneq]
Rmult_1_r [in Coq.Reals.RIneq]
Rmult_ne [in Coq.Reals.RIneq]
Rmult_0_l [in Coq.Reals.RIneq]
Rmult_0_r [in Coq.Reals.RIneq]
rmul_reg_l [in Coq.setoid_ring.Field_theory]
Rmul_0_l [in Coq.setoid_ring.Ring_theory]
Rneq_0_1 [in Coq.micromega.OrderedRing]
Rneq_symm [in Coq.micromega.OrderedRing]
Rnot_lt_ge [in Coq.Reals.RIneq]
Rnot_gt_ge [in Coq.Reals.RIneq]
Rnot_gt_le [in Coq.Reals.RIneq]
Rnot_lt_le [in Coq.Reals.RIneq]
Rnot_ge_lt [in Coq.Reals.RIneq]
Rnot_le_gt [in Coq.Reals.RIneq]
Rnot_ge_gt [in Coq.Reals.RIneq]
Rnot_le_lt [in Coq.Reals.RIneq]
Rolle [in Coq.Reals.MVT]
Ropp_div [in Coq.Reals.RIneq]
Ropp_ge_cancel [in Coq.Reals.RIneq]
Ropp_le_cancel [in Coq.Reals.RIneq]
Ropp_gt_cancel [in Coq.Reals.RIneq]
Ropp_lt_cancel [in Coq.Reals.RIneq]
Ropp_0_ge_le_contravar [in Coq.Reals.RIneq]
Ropp_0_le_ge_contravar [in Coq.Reals.RIneq]
Ropp_gt_lt_0_contravar [in Coq.Reals.RIneq]
Ropp_lt_gt_0_contravar [in Coq.Reals.RIneq]
Ropp_0_gt_lt_contravar [in Coq.Reals.RIneq]
Ropp_0_lt_gt_contravar [in Coq.Reals.RIneq]
Ropp_ge_contravar [in Coq.Reals.RIneq]
Ropp_le_contravar [in Coq.Reals.RIneq]
Ropp_ge_le_contravar [in Coq.Reals.RIneq]
Ropp_le_ge_contravar [in Coq.Reals.RIneq]
Ropp_gt_contravar [in Coq.Reals.RIneq]
Ropp_lt_contravar [in Coq.Reals.RIneq]
Ropp_lt_gt_contravar [in Coq.Reals.RIneq]
Ropp_gt_lt_contravar [in Coq.Reals.RIneq]
Ropp_inv_permute [in Coq.Reals.RIneq]
Ropp_minus_distr' [in Coq.Reals.RIneq]
Ropp_minus_distr [in Coq.Reals.RIneq]
Ropp_mult_distr_r_reverse [in Coq.Reals.RIneq]
Ropp_mult_distr_r [in Coq.Reals.RIneq]
Ropp_mult_distr_l_reverse [in Coq.Reals.RIneq]
Ropp_mult_distr_l [in Coq.Reals.RIneq]
Ropp_plus_distr [in Coq.Reals.RIneq]
Ropp_neq_0_compat [in Coq.Reals.RIneq]
Ropp_involutive [in Coq.Reals.RIneq]
Ropp_eq_0_compat [in Coq.Reals.RIneq]
Ropp_0 [in Coq.Reals.RIneq]
Ropp_eq_compat [in Coq.Reals.RIneq]
ropp_neq_0 [in Coq.setoid_ring.Field_theory]
Ropp_Rmin [in Coq.Reals.Rbasic_fun]
Ropp_Rmax [in Coq.Reals.Rbasic_fun]
Ropp_neg_pos [in Coq.micromega.OrderedRing]
Ropp_pos_neg [in Coq.micromega.OrderedRing]
Ropp_lt_mono [in Coq.micromega.OrderedRing]
Ropp_div [in Coq.Reals.Ratan]
Ropp_opp [in Coq.setoid_ring.Ring_theory]
Ropp_add [in Coq.setoid_ring.Ring_theory]
Ropp_mul_l [in Coq.setoid_ring.Ring_theory]
rotation_PI2 [in Coq.Reals.Rgeom]
rotation_0 [in Coq.Reals.Rgeom]
Rplus_sqr_eq_0 [in Coq.Reals.RIneq]
Rplus_sqr_eq_0_l [in Coq.Reals.RIneq]
Rplus_gt_reg_neg_r [in Coq.Reals.RIneq]
Rplus_ge_reg_neg_r [in Coq.Reals.RIneq]
Rplus_lt_reg_pos_r [in Coq.Reals.RIneq]
Rplus_le_reg_pos_r [in Coq.Reals.RIneq]
Rplus_ge_reg_l [in Coq.Reals.RIneq]
Rplus_gt_reg_l [in Coq.Reals.RIneq]
Rplus_le_reg_r [in Coq.Reals.RIneq]
Rplus_le_reg_l [in Coq.Reals.RIneq]
Rplus_lt_reg_r [in Coq.Reals.RIneq]
Rplus_lt_reg_l [in Coq.Reals.RIneq]
Rplus_le_le_0_compat [in Coq.Reals.RIneq]
Rplus_lt_le_0_compat [in Coq.Reals.RIneq]
Rplus_le_lt_0_compat [in Coq.Reals.RIneq]
Rplus_lt_0_compat [in Coq.Reals.RIneq]
Rplus_ge_gt_compat [in Coq.Reals.RIneq]
Rplus_gt_ge_compat [in Coq.Reals.RIneq]
Rplus_le_lt_compat [in Coq.Reals.RIneq]
Rplus_lt_le_compat [in Coq.Reals.RIneq]
Rplus_ge_compat [in Coq.Reals.RIneq]
Rplus_gt_compat [in Coq.Reals.RIneq]
Rplus_le_compat [in Coq.Reals.RIneq]
Rplus_lt_compat [in Coq.Reals.RIneq]
Rplus_ge_compat_r [in Coq.Reals.RIneq]
Rplus_le_compat_r [in Coq.Reals.RIneq]
Rplus_ge_compat_l [in Coq.Reals.RIneq]
Rplus_le_compat_l [in Coq.Reals.RIneq]
Rplus_gt_compat_r [in Coq.Reals.RIneq]
Rplus_lt_compat_r [in Coq.Reals.RIneq]
Rplus_gt_compat_l [in Coq.Reals.RIneq]
Rplus_minus [in Coq.Reals.RIneq]
Rplus_eq_R0 [in Coq.Reals.RIneq]
Rplus_eq_0_l [in Coq.Reals.RIneq]
Rplus_0_r_uniq [in Coq.Reals.RIneq]
Rplus_eq_reg_r [in Coq.Reals.RIneq]
Rplus_eq_reg_l [in Coq.Reals.RIneq]
Rplus_eq_compat_r [in Coq.Reals.RIneq]
Rplus_eq_compat_l [in Coq.Reals.RIneq]
Rplus_opp_r_uniq [in Coq.Reals.RIneq]
Rplus_opp_l [in Coq.Reals.RIneq]
Rplus_ne [in Coq.Reals.RIneq]
Rplus_0_r [in Coq.Reals.RIneq]
Rplus_contains_R [in Coq.Sets.Relations_2_facts]
Rplus_nonneg_nonneg [in Coq.micromega.OrderedRing]
Rplus_nonneg_pos [in Coq.micromega.OrderedRing]
Rplus_pos_nonneg [in Coq.micromega.OrderedRing]
Rplus_pos_pos [in Coq.micromega.OrderedRing]
Rplus_le_lt_mono [in Coq.micromega.OrderedRing]
Rplus_lt_le_mono [in Coq.micromega.OrderedRing]
Rplus_le_mono [in Coq.micromega.OrderedRing]
Rplus_lt_mono [in Coq.micromega.OrderedRing]
Rplus_lt_mono_r [in Coq.micromega.OrderedRing]
Rplus_lt_mono_l [in Coq.micromega.OrderedRing]
Rplus_le_mono_r [in Coq.micromega.OrderedRing]
Rplus_le_mono_l [in Coq.micromega.OrderedRing]
Rplus_cancel_l [in Coq.micromega.OrderedRing]
Rplus_comm [in Coq.micromega.OrderedRing]
Rplus_0_r [in Coq.micromega.OrderedRing]
Rplus_0_l [in Coq.micromega.OrderedRing]
Rpower_mult_distr [in Coq.Reals.Rpower]
Rpower_Ropp [in Coq.Reals.Rpower]
Rpower_sqrt [in Coq.Reals.Rpower]
Rpower_lt [in Coq.Reals.Rpower]
Rpower_pow [in Coq.Reals.Rpower]
Rpower_1 [in Coq.Reals.Rpower]
Rpower_O [in Coq.Reals.Rpower]
Rpower_mult [in Coq.Reals.Rpower]
Rpower_plus [in Coq.Reals.Rpower]
RPow_abs [in Coq.Reals.Rfunctions]
Rpow_mult_distr [in Coq.Reals.Rfunctions]
rrefl [in Coq.ssr.ssrfun]
Rsepare [in Coq.Reals.Rtopology]
Rseries_CV_comp [in Coq.Reals.SeqSeries]
Rset [in Coq.nsatz.Nsatz]
Rsor [in Coq.micromega.RMicromega]
Rsqrt_Rsqrt [in Coq.Reals.Rsqrt_def]
Rsqrt_positivity [in Coq.Reals.Rsqrt_def]
Rsqrt_exists [in Coq.Reals.Rsqrt_def]
Rsqr_0_uniq [in Coq.Reals.RIneq]
Rsqr_0 [in Coq.Reals.RIneq]
Rsqr_sin_cos_d_one [in Coq.Reals.Rtrigo_calc]
Rsqr_eq [in Coq.Reals.R_sqr]
Rsqr_inv [in Coq.Reals.R_sqr]
Rsqr_eq_asb_1 [in Coq.Reals.R_sqr]
Rsqr_eq_abs_0 [in Coq.Reals.R_sqr]
Rsqr_inj [in Coq.Reals.R_sqr]
Rsqr_lt_abs_1 [in Coq.Reals.R_sqr]
Rsqr_lt_abs_0 [in Coq.Reals.R_sqr]
Rsqr_le_abs_1 [in Coq.Reals.R_sqr]
Rsqr_le_abs_0 [in Coq.Reals.R_sqr]
Rsqr_abs [in Coq.Reals.R_sqr]
Rsqr_neg_pos_le_1 [in Coq.Reals.R_sqr]
Rsqr_neg_pos_le_0 [in Coq.Reals.R_sqr]
Rsqr_incrst_1 [in Coq.Reals.R_sqr]
Rsqr_incrst_0 [in Coq.Reals.R_sqr]
Rsqr_incr_1 [in Coq.Reals.R_sqr]
Rsqr_incr_0_var [in Coq.Reals.R_sqr]
Rsqr_incr_0 [in Coq.Reals.R_sqr]
Rsqr_plus_minus [in Coq.Reals.R_sqr]
Rsqr_minus_plus [in Coq.Reals.R_sqr]
Rsqr_eq_0 [in Coq.Reals.R_sqr]
Rsqr_div [in Coq.Reals.R_sqr]
Rsqr_pos_lt [in Coq.Reals.R_sqr]
Rsqr_gt_0_0 [in Coq.Reals.R_sqr]
Rsqr_1 [in Coq.Reals.R_sqr]
Rsqr_neg_minus [in Coq.Reals.R_sqr]
Rsqr_minus [in Coq.Reals.R_sqr]
Rsqr_plus [in Coq.Reals.R_sqr]
Rsqr_mult [in Coq.Reals.R_sqr]
Rsqr_neg [in Coq.Reals.R_sqr]
Rsqr_pow2 [in Coq.Reals.Rfunctions]
Rsqr_sol_eq_0_0 [in Coq.Reals.R_sqrt]
Rsqr_sol_eq_0_1 [in Coq.Reals.R_sqrt]
Rsqr_sqrt [in Coq.Reals.R_sqrt]
RstarRplus_RRstar [in Coq.Sets.Relations_2_facts]
Rstar_imp_coherent [in Coq.Sets.Relations_3_facts]
Rstar_equiv_Rstar1 [in Coq.Sets.Relations_2_facts]
Rstar_cases [in Coq.Sets.Relations_2_facts]
Rstar_transitive [in Coq.Sets.Relations_2_facts]
Rstar_contains_Rplus [in Coq.Sets.Relations_2_facts]
Rstar_contains_R [in Coq.Sets.Relations_2_facts]
Rstar_reflexive [in Coq.Sets.Relations_2_facts]
Rsth [in Coq.setoid_ring.Rings_R]
Rsth [in Coq.nsatz.Nsatz]
rsub_0_r [in Coq.setoid_ring.Field_theory]
rsub_0_l [in Coq.setoid_ring.Field_theory]
Rsum_abs [in Coq.Reals.PartSum]
Rsym_imp_notRsym [in Coq.Sets.Relations_1_facts]
Rsym_imp_Rstarsym [in Coq.Sets.Relations_2_facts]
RTautoChecker_sound [in Coq.micromega.RMicromega]
RTheory [in Coq.setoid_ring.RealField]
Rth_ARth [in Coq.setoid_ring.Ring_theory]
Rtimes_neq_0 [in Coq.micromega.OrderedRing]
Rtimes_square_nonneg [in Coq.micromega.OrderedRing]
Rtimes_neg_neg [in Coq.micromega.OrderedRing]
Rtimes_pos_neg [in Coq.micromega.OrderedRing]
Rtimes_nonneg_nonneg [in Coq.micromega.OrderedRing]
Rtimes_pos_pos [in Coq.micromega.OrderedRing]
Rtimes_comm [in Coq.micromega.OrderedRing]
Rtimes_0_l [in Coq.micromega.OrderedRing]
Rtimes_0_r [in Coq.micromega.OrderedRing]
Rtotal_order [in Coq.Reals.RIneq]
rt1n_ind_right [in Coq.Relations.Operators_Properties]
RWeakChecker_sound [in Coq.micromega.RMicromega]
rwP [in Coq.ssr.ssrbool]
rwP2 [in Coq.ssr.ssrbool]
R_rm [in Coq.Reals.RIneq]
R_power_theory [in Coq.setoid_ring.RealField]
R_sanity [in Coq.Vectors.Fin]
R_one_zero [in Coq.setoid_ring.Rings_R]
R_dist_mult_l [in Coq.Reals.Rfunctions]
R_dist_plus [in Coq.Reals.Rfunctions]
R_dist_tri [in Coq.Reals.Rfunctions]
R_dist_eq [in Coq.Reals.Rfunctions]
R_dist_refl [in Coq.Reals.Rfunctions]
R_dist_sym [in Coq.Reals.Rfunctions]
R_dist_pos [in Coq.Reals.Rfunctions]
R_one_zero [in Coq.nsatz.Nsatz]
R_power_theory [in Coq.nsatz.Nsatz]
R_as_OT.le_lteq [in Coq.Reals.ROrderedType]
r_list_pow_rev [in Coq.setoid_ring.Ring_polynom]
R_complete [in Coq.Reals.Rcomplete]
R.minus_min_distr_r [in Coq.Reals.Rminmax]
R.minus_min_distr_l [in Coq.Reals.Rminmax]
R.minus_max_distr_r [in Coq.Reals.Rminmax]
R.minus_max_distr_l [in Coq.Reals.Rminmax]
R.opp_min_distr [in Coq.Reals.Rminmax]
R.opp_max_distr [in Coq.Reals.Rminmax]
R.plus_min_distr_r [in Coq.Reals.Rminmax]
R.plus_min_distr_l [in Coq.Reals.Rminmax]
R.plus_max_distr_r [in Coq.Reals.Rminmax]
R.plus_max_distr_l [in Coq.Reals.Rminmax]
R0_fp_O [in Coq.Reals.R_Ifp]
R1_sqrt2_neq_0 [in Coq.Reals.Rtrigo_calc]
| 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 | (21801 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 | (910 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 | (729 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |