| 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 | (70451 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |
P (lemma)
P [in Coq.Numbers.Cyclic.Int63.Cyclic63]PaddCl_ok [in Coq.setoid_ring.Ncring_polynom]
PaddC_ok [in Coq.setoid_ring.Ring_polynom]
PaddC_ok [in Coq.micromega.EnvRing]
PaddXPX [in Coq.setoid_ring.Ncring_polynom]
PaddX_ok [in Coq.setoid_ring.Ring_polynom]
PaddX_ok [in Coq.micromega.EnvRing]
PaddX_ok [in Coq.setoid_ring.Ncring_polynom]
PaddX_ok2 [in Coq.setoid_ring.Ncring_polynom]
Padd_ok [in Coq.setoid_ring.Ring_polynom]
Padd_ok [in Coq.micromega.EnvRing]
Padd_ok [in Coq.setoid_ring.Ncring_polynom]
PairDecidableType.eq_trans [in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_sym [in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_refl [in Coq.Structures.DecidableTypeEx]
PairOrderedType.compare_spec [in Coq.Structures.OrdersEx]
PairOrderedType.eq_trans [in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_sym [in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_refl [in Coq.Structures.OrderedTypeEx]
PairOrderedType.lt_not_eq [in Coq.Structures.OrderedTypeEx]
PairOrderedType.lt_trans [in Coq.Structures.OrderedTypeEx]
pair_andP [in Coq.ssr.ssrbool]
pair_equal_spec [in Coq.Init.Datatypes]
Pand_semantics [in Coq.NArith.Ndigits]
PartialOrder_inverse [in Coq.Classes.RelationClasses]
PartialOrder_StrictOrder [in Coq.Classes.Morphisms]
PartialOrder_StrictOrder [in Coq.Classes.CMorphisms]
PartialOrder_inverse [in Coq.Classes.CRelationClasses]
partition_inv_nil [in Coq.Lists.List]
partition_length [in Coq.Lists.List]
partition_cons2 [in Coq.Lists.List]
partition_cons1 [in Coq.Lists.List]
pascal [in Coq.Reals.Binomial]
pascal_step3 [in Coq.Reals.Binomial]
pascal_step2 [in Coq.Reals.Binomial]
pascal_step1 [in Coq.Reals.Binomial]
Pbit_faithful [in Coq.NArith.Ndigits]
Pbit_faithful_0 [in Coq.NArith.Ndigits]
Pbit_Ptestbit [in Coq.NArith.Ndigits]
pcan_pcomp [in Coq.ssr.ssrfun]
pcan_inj [in Coq.ssr.ssrfun]
Pcompare_Eq_eq [in Coq.PArith.BinPos]
Pcompare_refl [in Coq.PArith.BinPos]
Pcompare_eq_Gt [in Coq.PArith.BinPos]
Pcompare_Peqb [in Coq.NArith.Ndec]
Pcond_Fnorm [in Coq.setoid_ring.Field_theory]
PCond_app [in Coq.setoid_ring.Field_theory]
PCond_cons_inv_r [in Coq.setoid_ring.Field_theory]
PCond_cons_inv_l [in Coq.setoid_ring.Field_theory]
PCond_cons [in Coq.setoid_ring.Field_theory]
Pdiff_semantics [in Coq.NArith.Ndigits]
Pdiv_eucl_remainder [in Coq.NArith.Ndiv_def]
Pdiv2 [in Coq.ZArith.Zdigits]
Peirce [in Coq.Logic.Classical_Prop]
PEpow_nz [in Coq.setoid_ring.Field_theory]
PEpow_mul_r [in Coq.setoid_ring.Field_theory]
PEpow_mul_l [in Coq.setoid_ring.Field_theory]
PEpow_add_r [in Coq.setoid_ring.Field_theory]
PEpow_1_l [in Coq.setoid_ring.Field_theory]
PEpow_1_r [in Coq.setoid_ring.Field_theory]
PEpow_0_r [in Coq.setoid_ring.Field_theory]
Peqb_true_eq [in Coq.PArith.BinPos]
Peqb_Pcompare [in Coq.NArith.Ndec]
Peqb_complete [in Coq.NArith.Ndec]
Peq_spec [in Coq.setoid_ring.Ring_polynom]
Peq_ok [in Coq.setoid_ring.Ring_polynom]
Peq_spec [in Coq.micromega.EnvRing]
Peq_ok [in Coq.micromega.EnvRing]
Peq_ok [in Coq.setoid_ring.Ncring_polynom]
PermutationA_preserves_NoDupA [in Coq.Lists.SetoidPermutation]
PermutationA_decompose [in Coq.Lists.SetoidPermutation]
PermutationA_equivlistA [in Coq.Lists.SetoidPermutation]
PermutationA_middle [in Coq.Lists.SetoidPermutation]
PermutationA_cons_app [in Coq.Lists.SetoidPermutation]
PermutationA_app_comm [in Coq.Lists.SetoidPermutation]
PermutationA_cons_append [in Coq.Lists.SetoidPermutation]
PermutationA_app_tail [in Coq.Lists.SetoidPermutation]
PermutationA_app_head [in Coq.Lists.SetoidPermutation]
permutation_map [in Coq.Sorting.PermutEq]
permutation_Permutation [in Coq.Sorting.PermutEq]
permutation_Permutation [in Coq.Sorting.PermutSetoid]
Permutation_impl_permutation [in Coq.Sorting.PermutSetoid]
Permutation_ind_transp [in Coq.Sorting.Permutation]
Permutation_Permutation_transp [in Coq.Sorting.Permutation]
Permutation_transp_cons [in Coq.Sorting.Permutation]
Permutation_nth [in Coq.Sorting.Permutation]
Permutation_nth_error_bis [in Coq.Sorting.Permutation]
Permutation_nth_error [in Coq.Sorting.Permutation]
Permutation_elt_map_inv [in Coq.Sorting.Permutation]
Permutation_image [in Coq.Sorting.Permutation]
Permutation_map_inv [in Coq.Sorting.Permutation]
Permutation_map [in Coq.Sorting.Permutation]
Permutation_repeat [in Coq.Sorting.Permutation]
Permutation_NoDup [in Coq.Sorting.Permutation]
Permutation_vs_cons_cons_inv [in Coq.Sorting.Permutation]
Permutation_vs_cons_inv [in Coq.Sorting.Permutation]
Permutation_vs_elt_inv [in Coq.Sorting.Permutation]
Permutation_length_2 [in Coq.Sorting.Permutation]
Permutation_length_2_inv [in Coq.Sorting.Permutation]
Permutation_length_1 [in Coq.Sorting.Permutation]
Permutation_length_1_inv [in Coq.Sorting.Permutation]
Permutation_app_inv_m [in Coq.Sorting.Permutation]
Permutation_app_inv_r [in Coq.Sorting.Permutation]
Permutation_app_inv_l [in Coq.Sorting.Permutation]
Permutation_cons_app_inv [in Coq.Sorting.Permutation]
Permutation_cons_inv [in Coq.Sorting.Permutation]
Permutation_app_inv [in Coq.Sorting.Permutation]
Permutation_Add_inv [in Coq.Sorting.Permutation]
Permutation_nil_app_cons [in Coq.Sorting.Permutation]
Permutation_ind_bis [in Coq.Sorting.Permutation]
Permutation_Forall2 [in Coq.Sorting.Permutation]
Permutation_length [in Coq.Sorting.Permutation]
Permutation_rev [in Coq.Sorting.Permutation]
Permutation_elt [in Coq.Sorting.Permutation]
Permutation_middle2 [in Coq.Sorting.Permutation]
Permutation_middle [in Coq.Sorting.Permutation]
Permutation_Add [in Coq.Sorting.Permutation]
Permutation_cons_app [in Coq.Sorting.Permutation]
Permutation_app_middle [in Coq.Sorting.Permutation]
Permutation_app_swap_app [in Coq.Sorting.Permutation]
Permutation_app_rot [in Coq.Sorting.Permutation]
Permutation_app_comm [in Coq.Sorting.Permutation]
Permutation_cons_append [in Coq.Sorting.Permutation]
Permutation_add_inside [in Coq.Sorting.Permutation]
Permutation_app [in Coq.Sorting.Permutation]
Permutation_app_head [in Coq.Sorting.Permutation]
Permutation_app_tail [in Coq.Sorting.Permutation]
Permutation_in [in Coq.Sorting.Permutation]
Permutation_morph_transp [in Coq.Sorting.Permutation]
Permutation_trans [in Coq.Sorting.Permutation]
Permutation_sym [in Coq.Sorting.Permutation]
Permutation_refl [in Coq.Sorting.Permutation]
Permutation_nil_cons [in Coq.Sorting.Permutation]
Permutation_nil [in Coq.Sorting.Permutation]
Permutation_PermutationA [in Coq.Lists.SetoidPermutation]
Permutation_eqlistA_commute [in Coq.Lists.SetoidPermutation]
permut_length [in Coq.Sorting.PermutEq]
permut_length_2 [in Coq.Sorting.PermutEq]
permut_length_1 [in Coq.Sorting.PermutEq]
permut_nil [in Coq.Sorting.PermutEq]
permut_cons_In [in Coq.Sorting.PermutEq]
permut_In_In [in Coq.Sorting.PermutEq]
permut_eqA [in Coq.Sorting.PermutSetoid]
permut_map [in Coq.Sorting.PermutSetoid]
permut_length [in Coq.Sorting.PermutSetoid]
permut_length_2 [in Coq.Sorting.PermutSetoid]
permut_length_1 [in Coq.Sorting.PermutSetoid]
permut_nil [in Coq.Sorting.PermutSetoid]
permut_cons_InA [in Coq.Sorting.PermutSetoid]
permut_InA_InA [in Coq.Sorting.PermutSetoid]
permut_remove_hd [in Coq.Sorting.PermutSetoid]
permut_remove_hd_eq [in Coq.Sorting.PermutSetoid]
permut_app_inv2 [in Coq.Sorting.PermutSetoid]
permut_app_inv1 [in Coq.Sorting.PermutSetoid]
permut_conv_inv [in Coq.Sorting.PermutSetoid]
permut_rev [in Coq.Sorting.PermutSetoid]
permut_sym_app [in Coq.Sorting.PermutSetoid]
permut_middle [in Coq.Sorting.PermutSetoid]
permut_add_cons_inside [in Coq.Sorting.PermutSetoid]
permut_add_cons_inside_eq [in Coq.Sorting.PermutSetoid]
permut_add_inside [in Coq.Sorting.PermutSetoid]
permut_add_inside_eq [in Coq.Sorting.PermutSetoid]
permut_app [in Coq.Sorting.PermutSetoid]
permut_cons [in Coq.Sorting.PermutSetoid]
permut_cons_eq [in Coq.Sorting.PermutSetoid]
permut_trans [in Coq.Sorting.PermutSetoid]
permut_sym [in Coq.Sorting.PermutSetoid]
permut_refl [in Coq.Sorting.PermutSetoid]
perm_left [in Coq.Sets.Permut]
perm_right [in Coq.Sets.Permut]
PEsimp_ok [in Coq.setoid_ring.Field_theory]
pexpr_times_nformula_correct [in Coq.micromega.RingMicromega]
PExpr_eq_spec [in Coq.setoid_ring.Field_theory]
PExpr_eq_semi_ok [in Coq.setoid_ring.Field_theory]
PE_1_r [in Coq.setoid_ring.Field_theory]
PE_1_l [in Coq.setoid_ring.Field_theory]
PFcons_fcons_inv [in Coq.setoid_ring.Field_theory]
PFcons0_fcons_inv [in Coq.setoid_ring.Field_theory]
PFcons00_fcons_inv [in Coq.setoid_ring.Field_theory]
PFcons1_fcons_inv [in Coq.setoid_ring.Field_theory]
PFcons2_fcons_inv [in Coq.setoid_ring.Field_theory]
phibis_aux_lowerbound [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_bounded [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_pos [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_equiv [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_nz [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_gcd [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv_negative [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_incr [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv_positive [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_positive_p2ibis [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_phi [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_phi_aux [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_incr [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_double [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_double_plus_one [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_lowerbound [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_bounded [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_nonneg [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn2 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn1 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_sequence_prop [in Coq.Reals.RiemannInt]
phi_pos1_succ [in Coq.micromega.ZCoeff]
phi_pos1_pos [in Coq.micromega.ZCoeff]
phi2_phi_inv2 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
Pigeonhole [in Coq.Sets.Image]
Pigeonhole_principle [in Coq.Sets.Image]
Pigeonhole_ter [in Coq.Sets.Infinite_sets]
Pigeonhole_bis [in Coq.Sets.Infinite_sets]
Piter_op_square [in Coq.ZArith.Zpow_alt]
Piter_mul_acc [in Coq.ZArith.Zpow_alt]
PI_neq0 [in Coq.Reals.Rtrigo1]
PI_4 [in Coq.Reals.Rtrigo1]
PI_RGT_0 [in Coq.Reals.Rtrigo1]
PI_2_3_7_ineq [in Coq.Reals.Machin]
PI_tg_cv [in Coq.Reals.AltSeries]
PI_tg_decreasing [in Coq.Reals.AltSeries]
PI_tg_pos [in Coq.Reals.AltSeries]
PI_ineq [in Coq.Reals.Ratan]
PI2_Rlt_PI [in Coq.Reals.Rtrigo1]
PI2_RGT_0 [in Coq.Reals.Rtrigo1]
pi2_int [in Coq.Reals.Rtrigo1]
PI2_1 [in Coq.Reals.Ratan]
PI2_3_2 [in Coq.Reals.Ratan]
PI2_lower_bound [in Coq.Reals.Ratan]
PI4_RLT_PI2 [in Coq.Reals.Rtrigo1]
PI4_RGT_0 [in Coq.Reals.Rtrigo_calc]
PI6_RLT_PI2 [in Coq.Reals.Rtrigo_calc]
PI6_RGT_0 [in Coq.Reals.Rtrigo_calc]
Pjump_pred_double [in Coq.micromega.EnvRing]
Pjump_xO_tail [in Coq.micromega.EnvRing]
Pjump_add [in Coq.micromega.EnvRing]
plus_minus [in Coq.Arith.Minus]
plus_frac_part2 [in Coq.Reals.R_Ifp]
plus_frac_part1 [in Coq.Reals.R_Ifp]
plus_Int_part2 [in Coq.Reals.R_Ifp]
plus_Int_part1 [in Coq.Reals.R_Ifp]
plus_Sn_m [in Coq.Init.Peano]
plus_n_Sm [in Coq.Init.Peano]
plus_O_n [in Coq.Init.Peano]
plus_n_O [in Coq.Init.Peano]
plus_tail_plus [in Coq.Arith.Plus]
plus_is_O [in Coq.Arith.Plus]
plus_lt_compat [in Coq.Arith.Plus]
plus_lt_le_compat [in Coq.Arith.Plus]
plus_le_lt_compat [in Coq.Arith.Plus]
plus_le_compat [in Coq.Arith.Plus]
plus_lt_compat_r [in Coq.Arith.Plus]
plus_lt_compat_l [in Coq.Arith.Plus]
plus_le_compat_r [in Coq.Arith.Plus]
plus_le_compat_l [in Coq.Arith.Plus]
plus_lt_reg_l [in Coq.Arith.Plus]
plus_le_reg_l [in Coq.Arith.Plus]
plus_reg_l [in Coq.Arith.Plus]
plus_assoc_reverse [in Coq.Arith.Plus]
plus_Rsqr_gt_0 [in Coq.Reals.Ratan]
plus_IZR [in Coq.Reals.RIneq]
plus_IZR_NEG_POS [in Coq.Reals.RIneq]
plus_INR [in Coq.Reals.RIneq]
plus_gt_compat_l [in Coq.Arith.Gt]
plus_gt_reg_l [in Coq.Arith.Gt]
plus_sum [in Coq.Reals.PartSum]
plus_IQR [in Coq.Reals.ClassicalConstructiveReals]
Pminus_mask_Gt [in Coq.PArith.BinPos]
PmulC_ok [in Coq.setoid_ring.Ring_polynom]
PmulC_aux_ok [in Coq.setoid_ring.Ring_polynom]
PmulC_ok [in Coq.micromega.EnvRing]
PmulC_aux_ok [in Coq.micromega.EnvRing]
PmulC_ok [in Coq.setoid_ring.Ncring_polynom]
PmulC_aux_ok [in Coq.setoid_ring.Ncring_polynom]
PmulI_ok [in Coq.setoid_ring.Ring_polynom]
PmulI_ok [in Coq.micromega.EnvRing]
Pmult_nat_r_plus_morphism [in Coq.PArith.Pnat]
Pmult_nat_plus_carry_morphism [in Coq.PArith.Pnat]
Pmult_nat_l_plus_morphism [in Coq.PArith.Pnat]
Pmult_nat_succ_morphism [in Coq.PArith.Pnat]
Pmult_nat_mult [in Coq.PArith.Pnat]
Pmul_ok [in Coq.setoid_ring.Ring_polynom]
Pmul_ok [in Coq.micromega.EnvRing]
Pmul_ok [in Coq.setoid_ring.Ncring_polynom]
PNSubstL_ok [in Coq.setoid_ring.Ring_polynom]
PNSubstL_ok [in Coq.micromega.EnvRing]
PNSubst_ok [in Coq.setoid_ring.Ring_polynom]
PNSubst_ok [in Coq.micromega.EnvRing]
PNSubst1_ok [in Coq.setoid_ring.Ring_polynom]
PNSubst1_ok [in Coq.micromega.EnvRing]
pointwise_pointwise [in Coq.Classes.Morphisms]
pointwise_pointwise [in Coq.Classes.CMorphisms]
point_in_holed_interval_works [in Coq.Reals.Runcountable]
poly [in Coq.Reals.Rfunctions]
poly_add_linear_compat [in Coq.btauto.Algebra]
poly_mul_valid_compat [in Coq.btauto.Algebra]
poly_mul_mon_valid_compat [in Coq.btauto.Algebra]
poly_mul_mon_null_compat [in Coq.btauto.Algebra]
poly_mul_cst_valid_compat [in Coq.btauto.Algebra]
poly_add_valid_compat [in Coq.btauto.Algebra]
poly_mul_compat [in Coq.btauto.Algebra]
poly_mul_mon_compat [in Coq.btauto.Algebra]
poly_mul_cst_compat [in Coq.btauto.Algebra]
poly_add_compat [in Coq.btauto.Algebra]
poly_of_formula_sound [in Coq.btauto.Reflect]
poly_of_formula_valid_compat [in Coq.btauto.Reflect]
poly_of_formula_eval_compat [in Coq.btauto.Reflect]
PolZadd_correct [in Coq.nsatz.NsatzTactic]
PolZeq_correct [in Coq.nsatz.NsatzTactic]
PolZmul_correct [in Coq.nsatz.NsatzTactic]
POneSubst_ok [in Coq.setoid_ring.Ring_polynom]
POneSubst_ok [in Coq.micromega.EnvRing]
Popp_ok [in Coq.setoid_ring.Ring_polynom]
Popp_ok [in Coq.micromega.EnvRing]
Popp_ok [in Coq.setoid_ring.Ncring_polynom]
pop2_bop2 [in Coq.micromega.QMicromega]
pop2_bop2 [in Coq.micromega.RMicromega]
pop2_bop2 [in Coq.micromega.ZMicromega]
Por_semantics [in Coq.NArith.Ndigits]
PositiveMapAdditionalFacts.gsident [in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.gsspec [in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.map2_commut [in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.xmap2_lr [in Coq.FSets.FMapPositive]
PositiveMap.add_3 [in Coq.FSets.FMapPositive]
PositiveMap.add_2 [in Coq.FSets.FMapPositive]
PositiveMap.add_1 [in Coq.FSets.FMapPositive]
PositiveMap.cardinal_1 [in Coq.FSets.FMapPositive]
PositiveMap.elements_3w [in Coq.FSets.FMapPositive]
PositiveMap.elements_3 [in Coq.FSets.FMapPositive]
PositiveMap.elements_2 [in Coq.FSets.FMapPositive]
PositiveMap.elements_1 [in Coq.FSets.FMapPositive]
PositiveMap.elements_complete [in Coq.FSets.FMapPositive]
PositiveMap.elements_correct [in Coq.FSets.FMapPositive]
PositiveMap.empty_1 [in Coq.FSets.FMapPositive]
PositiveMap.Empty_Node [in Coq.FSets.FMapPositive]
PositiveMap.Empty_alt [in Coq.FSets.FMapPositive]
PositiveMap.equal_2 [in Coq.FSets.FMapPositive]
PositiveMap.equal_1 [in Coq.FSets.FMapPositive]
PositiveMap.find_2 [in Coq.FSets.FMapPositive]
PositiveMap.find_1 [in Coq.FSets.FMapPositive]
PositiveMap.find_xfind_h [in Coq.FSets.FMapPositive]
PositiveMap.fold_1 [in Coq.FSets.FMapPositive]
PositiveMap.gempty [in Coq.FSets.FMapPositive]
PositiveMap.gleaf [in Coq.FSets.FMapPositive]
PositiveMap.gmapi [in Coq.FSets.FMapPositive]
PositiveMap.gmap2 [in Coq.FSets.FMapPositive]
PositiveMap.gro [in Coq.FSets.FMapPositive]
PositiveMap.grs [in Coq.FSets.FMapPositive]
PositiveMap.gso [in Coq.FSets.FMapPositive]
PositiveMap.gss [in Coq.FSets.FMapPositive]
PositiveMap.is_empty_2 [in Coq.FSets.FMapPositive]
PositiveMap.is_empty_1 [in Coq.FSets.FMapPositive]
PositiveMap.mapi_2 [in Coq.FSets.FMapPositive]
PositiveMap.mapi_1 [in Coq.FSets.FMapPositive]
PositiveMap.MapsTo_1 [in Coq.FSets.FMapPositive]
PositiveMap.map_2 [in Coq.FSets.FMapPositive]
PositiveMap.map_1 [in Coq.FSets.FMapPositive]
PositiveMap.map2_2 [in Coq.FSets.FMapPositive]
PositiveMap.map2_1 [in Coq.FSets.FMapPositive]
PositiveMap.mem_2 [in Coq.FSets.FMapPositive]
PositiveMap.mem_1 [in Coq.FSets.FMapPositive]
PositiveMap.mem_find [in Coq.FSets.FMapPositive]
PositiveMap.remove_3 [in Coq.FSets.FMapPositive]
PositiveMap.remove_2 [in Coq.FSets.FMapPositive]
PositiveMap.remove_1 [in Coq.FSets.FMapPositive]
PositiveMap.rleaf [in Coq.FSets.FMapPositive]
PositiveMap.xelements_sort [in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_2 [in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_1 [in Coq.FSets.FMapPositive]
PositiveMap.xelements_complete [in Coq.FSets.FMapPositive]
PositiveMap.xelements_ho [in Coq.FSets.FMapPositive]
PositiveMap.xelements_hi [in Coq.FSets.FMapPositive]
PositiveMap.xelements_oh [in Coq.FSets.FMapPositive]
PositiveMap.xelements_ih [in Coq.FSets.FMapPositive]
PositiveMap.xelements_oi [in Coq.FSets.FMapPositive]
PositiveMap.xelements_oo [in Coq.FSets.FMapPositive]
PositiveMap.xelements_io [in Coq.FSets.FMapPositive]
PositiveMap.xelements_ii [in Coq.FSets.FMapPositive]
PositiveMap.xelements_correct [in Coq.FSets.FMapPositive]
PositiveMap.xfind_left [in Coq.FSets.FMapPositive]
PositiveMap.xfoldi_1 [in Coq.FSets.FMapPositive]
PositiveMap.xgmapi [in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_r [in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_l [in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt_trans [in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt_antirefl [in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt_antirefl [in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.bits_lt_trans [in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.compare_spec [in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.eq_dec [in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt_not_eq [in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt_trans [in Coq.Structures.OrderedTypeEx]
PositiveSet.add_3 [in Coq.FSets.FSetPositive]
PositiveSet.add_2 [in Coq.FSets.FSetPositive]
PositiveSet.add_1 [in Coq.FSets.FSetPositive]
PositiveSet.add_spec [in Coq.FSets.FSetPositive]
PositiveSet.add_spec [in Coq.MSets.MSetPositive]
PositiveSet.cardinal_1 [in Coq.FSets.FSetPositive]
PositiveSet.cardinal_spec [in Coq.MSets.MSetPositive]
PositiveSet.choose_3 [in Coq.FSets.FSetPositive]
PositiveSet.choose_3' [in Coq.FSets.FSetPositive]
PositiveSet.choose_empty [in Coq.FSets.FSetPositive]
PositiveSet.choose_2 [in Coq.FSets.FSetPositive]
PositiveSet.choose_1 [in Coq.FSets.FSetPositive]
PositiveSet.choose_spec3 [in Coq.MSets.MSetPositive]
PositiveSet.choose_spec3' [in Coq.MSets.MSetPositive]
PositiveSet.choose_empty [in Coq.MSets.MSetPositive]
PositiveSet.choose_spec2 [in Coq.MSets.MSetPositive]
PositiveSet.choose_spec1 [in Coq.MSets.MSetPositive]
PositiveSet.compare [in Coq.FSets.FSetPositive]
PositiveSet.compare_x_empty [in Coq.FSets.FSetPositive]
PositiveSet.compare_empty_x [in Coq.FSets.FSetPositive]
PositiveSet.compare_x_Leaf [in Coq.FSets.FSetPositive]
PositiveSet.compare_eq [in Coq.FSets.FSetPositive]
PositiveSet.compare_gt [in Coq.FSets.FSetPositive]
PositiveSet.compare_equal [in Coq.FSets.FSetPositive]
PositiveSet.compare_bool_Eq [in Coq.FSets.FSetPositive]
PositiveSet.compare_inv [in Coq.FSets.FSetPositive]
PositiveSet.compare_bool_inv [in Coq.FSets.FSetPositive]
PositiveSet.compare_x_empty [in Coq.MSets.MSetPositive]
PositiveSet.compare_empty_x [in Coq.MSets.MSetPositive]
PositiveSet.compare_x_Leaf [in Coq.MSets.MSetPositive]
PositiveSet.compare_spec [in Coq.MSets.MSetPositive]
PositiveSet.compare_eq [in Coq.MSets.MSetPositive]
PositiveSet.compare_gt [in Coq.MSets.MSetPositive]
PositiveSet.compare_equal [in Coq.MSets.MSetPositive]
PositiveSet.compare_bool_Eq [in Coq.MSets.MSetPositive]
PositiveSet.compare_inv [in Coq.MSets.MSetPositive]
PositiveSet.compare_bool_inv [in Coq.MSets.MSetPositive]
PositiveSet.ct_compare_fun [in Coq.FSets.FSetPositive]
PositiveSet.ct_compare_bool [in Coq.FSets.FSetPositive]
PositiveSet.ct_lex [in Coq.FSets.FSetPositive]
PositiveSet.ct_xgg [in Coq.FSets.FSetPositive]
PositiveSet.ct_xll [in Coq.FSets.FSetPositive]
PositiveSet.ct_gxg [in Coq.FSets.FSetPositive]
PositiveSet.ct_lxl [in Coq.FSets.FSetPositive]
PositiveSet.ct_xce [in Coq.FSets.FSetPositive]
PositiveSet.ct_cxe [in Coq.FSets.FSetPositive]
PositiveSet.ct_compare [in Coq.MSets.MSetPositive]
PositiveSet.ct_compare_bool [in Coq.MSets.MSetPositive]
PositiveSet.ct_lex [in Coq.MSets.MSetPositive]
PositiveSet.ct_xgg [in Coq.MSets.MSetPositive]
PositiveSet.ct_xll [in Coq.MSets.MSetPositive]
PositiveSet.ct_gxg [in Coq.MSets.MSetPositive]
PositiveSet.ct_lxl [in Coq.MSets.MSetPositive]
PositiveSet.ct_xce [in Coq.MSets.MSetPositive]
PositiveSet.ct_cxe [in Coq.MSets.MSetPositive]
PositiveSet.diff_3 [in Coq.FSets.FSetPositive]
PositiveSet.diff_2 [in Coq.FSets.FSetPositive]
PositiveSet.diff_1 [in Coq.FSets.FSetPositive]
PositiveSet.diff_spec [in Coq.FSets.FSetPositive]
PositiveSet.diff_spec [in Coq.MSets.MSetPositive]
PositiveSet.elements_3w [in Coq.FSets.FSetPositive]
PositiveSet.elements_3 [in Coq.FSets.FSetPositive]
PositiveSet.elements_2 [in Coq.FSets.FSetPositive]
PositiveSet.elements_1 [in Coq.FSets.FSetPositive]
PositiveSet.elements_spec2w [in Coq.MSets.MSetPositive]
PositiveSet.elements_spec2 [in Coq.MSets.MSetPositive]
PositiveSet.elements_spec1 [in Coq.MSets.MSetPositive]
PositiveSet.empty_1 [in Coq.FSets.FSetPositive]
PositiveSet.empty_spec [in Coq.MSets.MSetPositive]
PositiveSet.equal_2 [in Coq.FSets.FSetPositive]
PositiveSet.equal_1 [in Coq.FSets.FSetPositive]
PositiveSet.equal_spec [in Coq.FSets.FSetPositive]
PositiveSet.equal_subset [in Coq.FSets.FSetPositive]
PositiveSet.equal_spec [in Coq.MSets.MSetPositive]
PositiveSet.equal_subset [in Coq.MSets.MSetPositive]
PositiveSet.eq_dec [in Coq.FSets.FSetPositive]
PositiveSet.eq_trans [in Coq.FSets.FSetPositive]
PositiveSet.eq_sym [in Coq.FSets.FSetPositive]
PositiveSet.eq_refl [in Coq.FSets.FSetPositive]
PositiveSet.eq_dec [in Coq.MSets.MSetPositive]
PositiveSet.exists_2 [in Coq.FSets.FSetPositive]
PositiveSet.exists_1 [in Coq.FSets.FSetPositive]
PositiveSet.exists_spec [in Coq.MSets.MSetPositive]
PositiveSet.filter_3 [in Coq.FSets.FSetPositive]
PositiveSet.filter_2 [in Coq.FSets.FSetPositive]
PositiveSet.filter_1 [in Coq.FSets.FSetPositive]
PositiveSet.filter_spec [in Coq.MSets.MSetPositive]
PositiveSet.fold_1 [in Coq.FSets.FSetPositive]
PositiveSet.fold_spec [in Coq.MSets.MSetPositive]
PositiveSet.for_all_2 [in Coq.FSets.FSetPositive]
PositiveSet.for_all_1 [in Coq.FSets.FSetPositive]
PositiveSet.for_all_spec [in Coq.MSets.MSetPositive]
PositiveSet.inter_3 [in Coq.FSets.FSetPositive]
PositiveSet.inter_2 [in Coq.FSets.FSetPositive]
PositiveSet.inter_1 [in Coq.FSets.FSetPositive]
PositiveSet.inter_spec [in Coq.FSets.FSetPositive]
PositiveSet.inter_spec [in Coq.MSets.MSetPositive]
PositiveSet.In_1 [in Coq.FSets.FSetPositive]
PositiveSet.is_empty_2 [in Coq.FSets.FSetPositive]
PositiveSet.is_empty_1 [in Coq.FSets.FSetPositive]
PositiveSet.is_empty_spec [in Coq.FSets.FSetPositive]
PositiveSet.is_empty_spec [in Coq.MSets.MSetPositive]
PositiveSet.lex_Eq [in Coq.FSets.FSetPositive]
PositiveSet.lex_Opp [in Coq.FSets.FSetPositive]
PositiveSet.lex_Eq [in Coq.MSets.MSetPositive]
PositiveSet.lex_Opp [in Coq.MSets.MSetPositive]
PositiveSet.lt_rev_append [in Coq.FSets.FSetPositive]
PositiveSet.lt_not_eq [in Coq.FSets.FSetPositive]
PositiveSet.lt_trans [in Coq.FSets.FSetPositive]
PositiveSet.lt_rev_append [in Coq.MSets.MSetPositive]
PositiveSet.max_elt_2 [in Coq.FSets.FSetPositive]
PositiveSet.max_elt_3 [in Coq.FSets.FSetPositive]
PositiveSet.max_elt_1 [in Coq.FSets.FSetPositive]
PositiveSet.max_elt_spec2 [in Coq.MSets.MSetPositive]
PositiveSet.max_elt_spec3 [in Coq.MSets.MSetPositive]
PositiveSet.max_elt_spec1 [in Coq.MSets.MSetPositive]
PositiveSet.mem_node [in Coq.FSets.FSetPositive]
PositiveSet.mem_Leaf [in Coq.FSets.FSetPositive]
PositiveSet.mem_2 [in Coq.FSets.FSetPositive]
PositiveSet.mem_1 [in Coq.FSets.FSetPositive]
PositiveSet.mem_node [in Coq.MSets.MSetPositive]
PositiveSet.mem_Leaf [in Coq.MSets.MSetPositive]
PositiveSet.mem_spec [in Coq.MSets.MSetPositive]
PositiveSet.min_elt_2 [in Coq.FSets.FSetPositive]
PositiveSet.min_elt_3 [in Coq.FSets.FSetPositive]
PositiveSet.min_elt_1 [in Coq.FSets.FSetPositive]
PositiveSet.min_elt_spec2 [in Coq.MSets.MSetPositive]
PositiveSet.min_elt_spec3 [in Coq.MSets.MSetPositive]
PositiveSet.min_elt_spec1 [in Coq.MSets.MSetPositive]
PositiveSet.partition_2 [in Coq.FSets.FSetPositive]
PositiveSet.partition_1 [in Coq.FSets.FSetPositive]
PositiveSet.partition_filter [in Coq.FSets.FSetPositive]
PositiveSet.partition_spec2 [in Coq.MSets.MSetPositive]
PositiveSet.partition_spec1 [in Coq.MSets.MSetPositive]
PositiveSet.partition_filter [in Coq.MSets.MSetPositive]
PositiveSet.remove_3 [in Coq.FSets.FSetPositive]
PositiveSet.remove_2 [in Coq.FSets.FSetPositive]
PositiveSet.remove_1 [in Coq.FSets.FSetPositive]
PositiveSet.remove_spec [in Coq.FSets.FSetPositive]
PositiveSet.remove_spec [in Coq.MSets.MSetPositive]
PositiveSet.singleton_2 [in Coq.FSets.FSetPositive]
PositiveSet.singleton_1 [in Coq.FSets.FSetPositive]
PositiveSet.singleton_spec [in Coq.MSets.MSetPositive]
PositiveSet.subset_2 [in Coq.FSets.FSetPositive]
PositiveSet.subset_1 [in Coq.FSets.FSetPositive]
PositiveSet.subset_spec [in Coq.FSets.FSetPositive]
PositiveSet.subset_Leaf_s [in Coq.FSets.FSetPositive]
PositiveSet.subset_spec [in Coq.MSets.MSetPositive]
PositiveSet.subset_Leaf_s [in Coq.MSets.MSetPositive]
PositiveSet.union_3 [in Coq.FSets.FSetPositive]
PositiveSet.union_2 [in Coq.FSets.FSetPositive]
PositiveSet.union_1 [in Coq.FSets.FSetPositive]
PositiveSet.union_spec [in Coq.FSets.FSetPositive]
PositiveSet.union_spec [in Coq.MSets.MSetPositive]
PositiveSet.xelements_spec [in Coq.FSets.FSetPositive]
PositiveSet.xelements_spec [in Coq.MSets.MSetPositive]
PositiveSet.xexists_spec [in Coq.FSets.FSetPositive]
PositiveSet.xexists_spec [in Coq.MSets.MSetPositive]
PositiveSet.xfilter_spec [in Coq.FSets.FSetPositive]
PositiveSet.xfilter_spec [in Coq.MSets.MSetPositive]
PositiveSet.xforall_spec [in Coq.FSets.FSetPositive]
PositiveSet.xforall_spec [in Coq.MSets.MSetPositive]
positive_to_int31_spec [in Coq.Numbers.Cyclic.Int31.Cyclic31]
positive_to_int31_phi_inv_positive [in Coq.Numbers.Cyclic.Int31.Cyclic31]
positive_derivative [in Coq.Reals.MVT]
Positive_as_OT.lt_not_eq [in Coq.Structures.OrderedTypeEx]
positive_to_int_spec [in Coq.Numbers.Cyclic.Int63.Cyclic63]
positive_nat_N [in Coq.ZArith.Znat]
positive_N_nat [in Coq.ZArith.Znat]
positive_N_Z [in Coq.ZArith.Znat]
positive_nat_Z [in Coq.ZArith.Znat]
posPartAbsMax [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Pospow_lin_le_2pow [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Pos_log2floor_plus1_spec_Qpower [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Pos_pred_double_inj [in Coq.Reals.Cauchy.ConstructiveExtra]
pos_mod_spec [in Coq.Numbers.Cyclic.Int63.Cyclic63]
pos_opp_lt [in Coq.Reals.Ratan]
pos_half_prf [in Coq.Reals.RIneq]
pos_INR [in Coq.Reals.RIneq]
pos_INR_nat_of_P [in Coq.Reals.RIneq]
pos_Rl_P2 [in Coq.Reals.RList]
pos_Rl_P1 [in Coq.Reals.RList]
pos_sum_more [in Coq.Reals.Abstract.ConstructiveSum]
pos_le_add [in Coq.micromega.ZMicromega]
Pos_pow_le_mono_r [in Coq.Reals.Cauchy.PosExtra]
Pos_le_multiple [in Coq.Reals.Cauchy.PosExtra]
Pos_pow_1_r [in Coq.Reals.Cauchy.PosExtra]
Pos_log2ceil_plus1_spec [in Coq.Reals.Cauchy.QExtra]
Pos_log2floor_plus1_spec [in Coq.Reals.Cauchy.QExtra]
pos_eq_refl [in Coq.rtauto.Rtauto]
Pos.add_min_distr_r [in Coq.PArith.BinPos]
Pos.add_min_distr_l [in Coq.PArith.BinPos]
Pos.add_max_distr_r [in Coq.PArith.BinPos]
Pos.add_max_distr_l [in Coq.PArith.BinPos]
Pos.add_sub_assoc [in Coq.PArith.BinPos]
Pos.add_sub [in Coq.PArith.BinPos]
Pos.add_le_mono [in Coq.PArith.BinPos]
Pos.add_le_mono_r [in Coq.PArith.BinPos]
Pos.add_le_mono_l [in Coq.PArith.BinPos]
Pos.add_lt_mono [in Coq.PArith.BinPos]
Pos.add_lt_mono_r [in Coq.PArith.BinPos]
Pos.add_lt_mono_l [in Coq.PArith.BinPos]
Pos.add_compare_mono_r [in Coq.PArith.BinPos]
Pos.add_compare_mono_l [in Coq.PArith.BinPos]
Pos.add_diag [in Coq.PArith.BinPos]
Pos.add_xO_pred_double [in Coq.PArith.BinPos]
Pos.add_xI_pred_double [in Coq.PArith.BinPos]
Pos.add_xO [in Coq.PArith.BinPos]
Pos.add_assoc [in Coq.PArith.BinPos]
Pos.add_carry_reg_l [in Coq.PArith.BinPos]
Pos.add_carry_reg_r [in Coq.PArith.BinPos]
Pos.add_cancel_l [in Coq.PArith.BinPos]
Pos.add_cancel_r [in Coq.PArith.BinPos]
Pos.add_reg_l [in Coq.PArith.BinPos]
Pos.add_reg_r [in Coq.PArith.BinPos]
Pos.add_carry_add [in Coq.PArith.BinPos]
Pos.add_no_neutral [in Coq.PArith.BinPos]
Pos.add_succ_l [in Coq.PArith.BinPos]
Pos.add_succ_r [in Coq.PArith.BinPos]
Pos.add_comm [in Coq.PArith.BinPos]
Pos.add_carry_spec [in Coq.PArith.BinPos]
Pos.add_1_l [in Coq.PArith.BinPos]
Pos.add_1_r [in Coq.PArith.BinPos]
Pos.compare_succ_succ [in Coq.PArith.BinPos]
Pos.compare_succ_l [in Coq.PArith.BinPos]
Pos.compare_succ_r [in Coq.PArith.BinPos]
Pos.compare_le_iff [in Coq.PArith.BinPos]
Pos.compare_lt_iff [in Coq.PArith.BinPos]
Pos.compare_antisym [in Coq.PArith.BinPos]
Pos.compare_eq_iff [in Coq.PArith.BinPos]
Pos.compare_cont_antisym [in Coq.PArith.BinPos]
Pos.compare_cont_refl [in Coq.PArith.BinPos]
Pos.compare_sub_mask [in Coq.PArith.BinPos]
Pos.compare_xO_xI [in Coq.PArith.BinPos]
Pos.compare_xI_xO [in Coq.PArith.BinPos]
Pos.compare_xI_xI [in Coq.PArith.BinPos]
Pos.compare_xO_xO [in Coq.PArith.BinPos]
Pos.compare_cont_Gt_not_Gt [in Coq.PArith.BinPos]
Pos.compare_cont_Gt_not_Lt [in Coq.PArith.BinPos]
Pos.compare_cont_Lt_not_Gt [in Coq.PArith.BinPos]
Pos.compare_cont_Lt_not_Lt [in Coq.PArith.BinPos]
Pos.compare_cont_Gt_Gt [in Coq.PArith.BinPos]
Pos.compare_cont_Gt_Lt [in Coq.PArith.BinPos]
Pos.compare_cont_Lt_Lt [in Coq.PArith.BinPos]
Pos.compare_cont_Lt_Gt [in Coq.PArith.BinPos]
Pos.compare_cont_Eq [in Coq.PArith.BinPos]
Pos.compare_cont_spec [in Coq.PArith.BinPos]
Pos.divide_mul_r [in Coq.PArith.BinPos]
Pos.divide_mul_l [in Coq.PArith.BinPos]
Pos.divide_xO_xO [in Coq.PArith.BinPos]
Pos.divide_xO_xI [in Coq.PArith.BinPos]
Pos.divide_add_cancel_l [in Coq.PArith.BinPos]
Pos.double_succ [in Coq.PArith.BinPos]
Pos.eqb_eq [in Coq.PArith.BinPos]
Pos.eq_dep_eq_positive [in Coq.PArith.BinPos]
Pos.eq_dec [in Coq.PArith.BinPos]
Pos.gcdn_greatest [in Coq.PArith.BinPos]
Pos.gcd_greatest [in Coq.PArith.BinPos]
Pos.gcd_divide_r [in Coq.PArith.BinPos]
Pos.gcd_divide_l [in Coq.PArith.BinPos]
Pos.ge_le [in Coq.PArith.BinPos]
Pos.ge_le_iff [in Coq.PArith.BinPos]
Pos.ggcdn_correct_divisors [in Coq.PArith.BinPos]
Pos.ggcdn_gcdn [in Coq.PArith.BinPos]
Pos.ggcd_greatest [in Coq.PArith.BinPos]
Pos.ggcd_correct_divisors [in Coq.PArith.BinPos]
Pos.ggcd_gcd [in Coq.PArith.BinPos]
Pos.gt_lt [in Coq.PArith.BinPos]
Pos.gt_lt_iff [in Coq.PArith.BinPos]
Pos.gt_iff_add [in Coq.PArith.BinPos]
Pos.iter_op_succ [in Coq.PArith.BinPos]
Pos.iter_invariant [in Coq.PArith.BinPos]
Pos.iter_ind [in Coq.PArith.BinPos]
Pos.iter_add [in Coq.PArith.BinPos]
Pos.iter_succ_r [in Coq.PArith.BinPos]
Pos.iter_succ [in Coq.PArith.BinPos]
Pos.iter_swap [in Coq.PArith.BinPos]
Pos.iter_swap_gen [in Coq.PArith.BinPos]
Pos.leb_le [in Coq.PArith.BinPos]
Pos.le_antisym [in Coq.PArith.BinPos]
Pos.le_succ_l [in Coq.PArith.BinPos]
Pos.le_trans [in Coq.PArith.BinPos]
Pos.le_lt_trans [in Coq.PArith.BinPos]
Pos.le_refl [in Coq.PArith.BinPos]
Pos.le_nlt [in Coq.PArith.BinPos]
Pos.le_1_l [in Coq.PArith.BinPos]
Pos.le_ge [in Coq.PArith.BinPos]
Pos.ltb_lt [in Coq.PArith.BinPos]
Pos.lt_not_add_l [in Coq.PArith.BinPos]
Pos.lt_add_r [in Coq.PArith.BinPos]
Pos.lt_add_diag_r [in Coq.PArith.BinPos]
Pos.lt_le_trans [in Coq.PArith.BinPos]
Pos.lt_total [in Coq.PArith.BinPos]
Pos.lt_ind [in Coq.PArith.BinPos]
Pos.lt_trans [in Coq.PArith.BinPos]
Pos.lt_lt_succ [in Coq.PArith.BinPos]
Pos.lt_le_incl [in Coq.PArith.BinPos]
Pos.lt_nle [in Coq.PArith.BinPos]
Pos.lt_1_succ [in Coq.PArith.BinPos]
Pos.lt_succ_diag_r [in Coq.PArith.BinPos]
Pos.lt_succ_r [in Coq.PArith.BinPos]
Pos.lt_gt [in Coq.PArith.BinPos]
Pos.lt_iff_add [in Coq.PArith.BinPos]
Pos.max_1_r [in Coq.PArith.BinPos]
Pos.max_1_l [in Coq.PArith.BinPos]
Pos.max_r [in Coq.PArith.BinPos]
Pos.max_l [in Coq.PArith.BinPos]
Pos.min_1_r [in Coq.PArith.BinPos]
Pos.min_1_l [in Coq.PArith.BinPos]
Pos.min_r [in Coq.PArith.BinPos]
Pos.min_l [in Coq.PArith.BinPos]
Pos.mul_min_distr_r [in Coq.PArith.BinPos]
Pos.mul_min_distr_l [in Coq.PArith.BinPos]
Pos.mul_max_distr_r [in Coq.PArith.BinPos]
Pos.mul_max_distr_l [in Coq.PArith.BinPos]
Pos.mul_sub_distr_r [in Coq.PArith.BinPos]
Pos.mul_sub_distr_l [in Coq.PArith.BinPos]
Pos.mul_le_mono [in Coq.PArith.BinPos]
Pos.mul_le_mono_r [in Coq.PArith.BinPos]
Pos.mul_le_mono_l [in Coq.PArith.BinPos]
Pos.mul_lt_mono [in Coq.PArith.BinPos]
Pos.mul_lt_mono_r [in Coq.PArith.BinPos]
Pos.mul_lt_mono_l [in Coq.PArith.BinPos]
Pos.mul_compare_mono_r [in Coq.PArith.BinPos]
Pos.mul_compare_mono_l [in Coq.PArith.BinPos]
Pos.mul_eq_1_r [in Coq.PArith.BinPos]
Pos.mul_eq_1_l [in Coq.PArith.BinPos]
Pos.mul_cancel_l [in Coq.PArith.BinPos]
Pos.mul_cancel_r [in Coq.PArith.BinPos]
Pos.mul_reg_l [in Coq.PArith.BinPos]
Pos.mul_reg_r [in Coq.PArith.BinPos]
Pos.mul_xO_discr [in Coq.PArith.BinPos]
Pos.mul_xI_mul_xO_discr [in Coq.PArith.BinPos]
Pos.mul_succ_r [in Coq.PArith.BinPos]
Pos.mul_succ_l [in Coq.PArith.BinPos]
Pos.mul_assoc [in Coq.PArith.BinPos]
Pos.mul_add_distr_r [in Coq.PArith.BinPos]
Pos.mul_add_distr_l [in Coq.PArith.BinPos]
Pos.mul_comm [in Coq.PArith.BinPos]
Pos.mul_xI_r [in Coq.PArith.BinPos]
Pos.mul_xO_r [in Coq.PArith.BinPos]
Pos.mul_1_r [in Coq.PArith.BinPos]
Pos.mul_1_l [in Coq.PArith.BinPos]
Pos.nlt_1_r [in Coq.PArith.BinPos]
Pos.of_nat_succ [in Coq.PArith.BinPos]
Pos.PeanoViewUnique [in Coq.PArith.BinPos]
Pos.peano_equiv [in Coq.PArith.BinPos]
Pos.peano_case [in Coq.PArith.BinPos]
Pos.peano_rect_base [in Coq.PArith.BinPos]
Pos.peano_rect_succ [in Coq.PArith.BinPos]
Pos.pow_gt_1 [in Coq.PArith.BinPos]
Pos.pow_succ_r [in Coq.PArith.BinPos]
Pos.pow_1_r [in Coq.PArith.BinPos]
Pos.pred_of_succ_nat [in Coq.PArith.BinPos]
Pos.pred_sub [in Coq.PArith.BinPos]
Pos.pred_N_succ [in Coq.PArith.BinPos]
Pos.pred_succ [in Coq.PArith.BinPos]
Pos.pred_double_xO_discr [in Coq.PArith.BinPos]
Pos.pred_double_succ [in Coq.PArith.BinPos]
Pos.pred_double_spec [in Coq.PArith.BinPos]
Pos.size_le [in Coq.PArith.BinPos]
Pos.size_gt [in Coq.PArith.BinPos]
Pos.size_nat_monotone [in Coq.PArith.BinPos]
Pos.sqrtrem_spec [in Coq.PArith.BinPos]
Pos.sqrtrem_step_spec [in Coq.PArith.BinPos]
Pos.sqrt_spec [in Coq.PArith.BinPos]
Pos.square_spec [in Coq.PArith.BinPos]
Pos.square_xI [in Coq.PArith.BinPos]
Pos.square_xO [in Coq.PArith.BinPos]
Pos.sub_diag [in Coq.PArith.BinPos]
Pos.sub_lt [in Coq.PArith.BinPos]
Pos.sub_le [in Coq.PArith.BinPos]
Pos.sub_mask_neg [in Coq.PArith.BinPos]
Pos.sub_mask_neg_iff' [in Coq.PArith.BinPos]
Pos.sub_xO_xI [in Coq.PArith.BinPos]
Pos.sub_xI_xO [in Coq.PArith.BinPos]
Pos.sub_xI_xI [in Coq.PArith.BinPos]
Pos.sub_xO_xO [in Coq.PArith.BinPos]
Pos.sub_sub_distr [in Coq.PArith.BinPos]
Pos.sub_add_distr [in Coq.PArith.BinPos]
Pos.sub_decr [in Coq.PArith.BinPos]
Pos.sub_lt_mono_r [in Coq.PArith.BinPos]
Pos.sub_compare_mono_r [in Coq.PArith.BinPos]
Pos.sub_compare_mono_l [in Coq.PArith.BinPos]
Pos.sub_lt_mono_l [in Coq.PArith.BinPos]
Pos.sub_add [in Coq.PArith.BinPos]
Pos.sub_mask_pos [in Coq.PArith.BinPos]
Pos.sub_mask_pos' [in Coq.PArith.BinPos]
Pos.sub_succ_r [in Coq.PArith.BinPos]
Pos.sub_1_r [in Coq.PArith.BinPos]
Pos.sub_mask_neg_iff [in Coq.PArith.BinPos]
Pos.sub_mask_add_diag_r [in Coq.PArith.BinPos]
Pos.sub_mask_pos_iff [in Coq.PArith.BinPos]
Pos.sub_mask_add_diag_l [in Coq.PArith.BinPos]
Pos.sub_mask_add [in Coq.PArith.BinPos]
Pos.sub_mask_diag [in Coq.PArith.BinPos]
Pos.sub_mask_nul_iff [in Coq.PArith.BinPos]
Pos.sub_mask_spec [in Coq.PArith.BinPos]
Pos.sub_mask_carry_spec [in Coq.PArith.BinPos]
Pos.sub_mask_succ_r [in Coq.PArith.BinPos]
Pos.succ_of_nat [in Coq.PArith.BinPos]
Pos.succ_min_distr [in Coq.PArith.BinPos]
Pos.succ_max_distr [in Coq.PArith.BinPos]
Pos.succ_le_mono [in Coq.PArith.BinPos]
Pos.succ_lt_mono [in Coq.PArith.BinPos]
Pos.succ_inj [in Coq.PArith.BinPos]
Pos.succ_pred [in Coq.PArith.BinPos]
Pos.succ_pred_or [in Coq.PArith.BinPos]
Pos.succ_not_1 [in Coq.PArith.BinPos]
Pos.succ_pred_double [in Coq.PArith.BinPos]
Pos.succ_discr [in Coq.PArith.BinPos]
Pos.xI_succ_xO [in Coq.PArith.BinPos]
Pos2Nat.id [in Coq.PArith.Pnat]
Pos2Nat.inj [in Coq.PArith.Pnat]
Pos2Nat.inj_iter [in Coq.PArith.Pnat]
Pos2Nat.inj_max [in Coq.PArith.Pnat]
Pos2Nat.inj_min [in Coq.PArith.Pnat]
Pos2Nat.inj_pred_max [in Coq.PArith.Pnat]
Pos2Nat.inj_pred [in Coq.PArith.Pnat]
Pos2Nat.inj_sub_max [in Coq.PArith.Pnat]
Pos2Nat.inj_sub [in Coq.PArith.Pnat]
Pos2Nat.inj_ge [in Coq.PArith.Pnat]
Pos2Nat.inj_gt [in Coq.PArith.Pnat]
Pos2Nat.inj_le [in Coq.PArith.Pnat]
Pos2Nat.inj_lt [in Coq.PArith.Pnat]
Pos2Nat.inj_compare [in Coq.PArith.Pnat]
Pos2Nat.inj_iff [in Coq.PArith.Pnat]
Pos2Nat.inj_xI [in Coq.PArith.Pnat]
Pos2Nat.inj_xO [in Coq.PArith.Pnat]
Pos2Nat.inj_1 [in Coq.PArith.Pnat]
Pos2Nat.inj_mul [in Coq.PArith.Pnat]
Pos2Nat.inj_add [in Coq.PArith.Pnat]
Pos2Nat.inj_succ [in Coq.PArith.Pnat]
Pos2Nat.is_pos [in Coq.PArith.Pnat]
Pos2Nat.is_succ [in Coq.PArith.Pnat]
Pos2SuccNat.id_succ [in Coq.PArith.Pnat]
Pos2SuccNat.pred_id [in Coq.PArith.Pnat]
Pos2Z_pos_is_pos [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Pos2Z.add_pos_pos [in Coq.ZArith.BinInt]
Pos2Z.add_neg_pos [in Coq.ZArith.BinInt]
Pos2Z.add_pos_neg [in Coq.ZArith.BinInt]
Pos2Z.add_neg_neg [in Coq.ZArith.BinInt]
Pos2Z.divide_pos_neg_l [in Coq.ZArith.BinInt]
Pos2Z.divide_pos_neg_r [in Coq.ZArith.BinInt]
Pos2Z.id [in Coq.ZArith.BinInt]
Pos2Z.inj [in Coq.ZArith.BinInt]
Pos2Z.inj_pos_iff [in Coq.ZArith.BinInt]
Pos2Z.inj_pos [in Coq.ZArith.BinInt]
Pos2Z.inj_neg_iff [in Coq.ZArith.BinInt]
Pos2Z.inj_neg [in Coq.ZArith.BinInt]
Pos2Z.inj_testbit [in Coq.ZArith.BinInt]
Pos2Z.inj_gcd [in Coq.ZArith.BinInt]
Pos2Z.inj_sqrt [in Coq.ZArith.BinInt]
Pos2Z.inj_min [in Coq.ZArith.BinInt]
Pos2Z.inj_max [in Coq.ZArith.BinInt]
Pos2Z.inj_eqb [in Coq.ZArith.BinInt]
Pos2Z.inj_ltb [in Coq.ZArith.BinInt]
Pos2Z.inj_leb [in Coq.ZArith.BinInt]
Pos2Z.inj_compare [in Coq.ZArith.BinInt]
Pos2Z.inj_square [in Coq.ZArith.BinInt]
Pos2Z.inj_pow [in Coq.ZArith.BinInt]
Pos2Z.inj_pow_pos [in Coq.ZArith.BinInt]
Pos2Z.inj_mul [in Coq.ZArith.BinInt]
Pos2Z.inj_pred [in Coq.ZArith.BinInt]
Pos2Z.inj_sub_max [in Coq.ZArith.BinInt]
Pos2Z.inj_sub [in Coq.ZArith.BinInt]
Pos2Z.inj_add [in Coq.ZArith.BinInt]
Pos2Z.inj_succ [in Coq.ZArith.BinInt]
Pos2Z.inj_xI [in Coq.ZArith.BinInt]
Pos2Z.inj_xO [in Coq.ZArith.BinInt]
Pos2Z.inj_1 [in Coq.ZArith.BinInt]
Pos2Z.inj_iff [in Coq.ZArith.BinInt]
Pos2Z.is_nonneg [in Coq.ZArith.BinInt]
Pos2Z.is_pos [in Coq.ZArith.BinInt]
Pos2Z.neg_xI [in Coq.ZArith.BinInt]
Pos2Z.neg_xO [in Coq.ZArith.BinInt]
Pos2Z.neg_lt_neg [in Coq.ZArith.BinInt]
Pos2Z.neg_le_neg [in Coq.ZArith.BinInt]
Pos2Z.neg_lt_pos [in Coq.ZArith.BinInt]
Pos2Z.neg_le_pos [in Coq.ZArith.BinInt]
Pos2Z.neg_is_nonpos [in Coq.ZArith.BinInt]
Pos2Z.neg_is_neg [in Coq.ZArith.BinInt]
Pos2Z.opp_pos [in Coq.ZArith.BinInt]
Pos2Z.opp_neg [in Coq.ZArith.BinInt]
Pos2Z.pos_xI [in Coq.ZArith.BinInt]
Pos2Z.pos_xO [in Coq.ZArith.BinInt]
Pos2Z.pos_lt_pos [in Coq.ZArith.BinInt]
Pos2Z.pos_le_pos [in Coq.ZArith.BinInt]
Pos2Z.pos_is_nonneg [in Coq.ZArith.BinInt]
Pos2Z.pos_is_pos [in Coq.ZArith.BinInt]
Pos2Z.testbit_pos [in Coq.ZArith.BinInt]
Pos2Z.testbit_neg [in Coq.ZArith.BinInt]
powerRZ_mult_distr [in Coq.Reals.Rfunctions]
powerRZ_neg [in Coq.Reals.Rfunctions]
powerRZ_inv [in Coq.Reals.Rfunctions]
powerRZ_ind [in Coq.Reals.Rfunctions]
powerRZ_R1 [in Coq.Reals.Rfunctions]
powerRZ_le [in Coq.Reals.Rfunctions]
powerRZ_lt [in Coq.Reals.Rfunctions]
powerRZ_add [in Coq.Reals.Rfunctions]
powerRZ_pos_sub [in Coq.Reals.Rfunctions]
powerRZ_NOR [in Coq.Reals.Rfunctions]
powerRZ_1 [in Coq.Reals.Rfunctions]
powerRZ_O [in Coq.Reals.Rfunctions]
powerRZ_Rpower [in Coq.Reals.Rpower]
Power_monotonic [in Coq.Reals.Rfunctions]
Power_set_Inhabited [in Coq.Sets.Powerset]
pow_i [in Coq.Reals.Rtrigo_def]
pow_powerRZ [in Coq.Reals.Rfunctions]
pow_maj_Rabs [in Coq.Reals.Rfunctions]
pow_Rabs [in Coq.Reals.Rfunctions]
pow_R1_Rle [in Coq.Reals.Rfunctions]
pow_incr [in Coq.Reals.Rfunctions]
pow_mult [in Coq.Reals.Rfunctions]
pow_1_abs [in Coq.Reals.Rfunctions]
pow_1_odd [in Coq.Reals.Rfunctions]
pow_1_even [in Coq.Reals.Rfunctions]
pow_le [in Coq.Reals.Rfunctions]
pow_Rsqr [in Coq.Reals.Rfunctions]
pow_R1 [in Coq.Reals.Rfunctions]
pow_lt_1_zero [in Coq.Reals.Rfunctions]
pow_ne_zero [in Coq.Reals.Rfunctions]
Pow_x_infinity [in Coq.Reals.Rfunctions]
pow_lt [in Coq.Reals.Rfunctions]
pow_RN_plus [in Coq.Reals.Rfunctions]
pow_nonzero [in Coq.Reals.Rfunctions]
pow_add [in Coq.Reals.Rfunctions]
pow_1 [in Coq.Reals.Rfunctions]
pow_O [in Coq.Reals.Rfunctions]
pow_pos_add [in Coq.setoid_ring.Ring_polynom]
pow_pos_add [in Coq.micromega.EnvRing]
pow_2_n_infty [in Coq.Reals.Rsqrt_def]
pow_2_n_growing [in Coq.Reals.Rsqrt_def]
pow_2_n_neq_R0 [in Coq.Reals.Rsqrt_def]
pow_pos_div [in Coq.setoid_ring.Field_theory]
pow_pos_nz [in Coq.setoid_ring.Field_theory]
pow_pos_mul_r [in Coq.setoid_ring.Field_theory]
pow_pos_add_r [in Coq.setoid_ring.Field_theory]
pow_pos_mul_l [in Coq.setoid_ring.Field_theory]
pow_pos_cst [in Coq.setoid_ring.Field_theory]
pow_pos_1 [in Coq.setoid_ring.Field_theory]
pow_pos_0 [in Coq.setoid_ring.Field_theory]
pow_not_zero [in Coq.setoid_ring.Integral_domain]
pow_lt_1_compat [in Coq.Reals.Ratan]
pow_N_pow_N [in Coq.setoid_ring.Ring_theory]
pow_pos_add [in Coq.setoid_ring.Ring_theory]
pow_pos_succ [in Coq.setoid_ring.Ring_theory]
pow_pos_swap [in Coq.setoid_ring.Ring_theory]
pow_IZR [in Coq.Reals.RIneq]
pow_INR [in Coq.Reals.RIneq]
pow_N_pow_N [in Coq.setoid_ring.Ncring]
pow_pos_add [in Coq.setoid_ring.Ncring]
pow_pos_succ [in Coq.setoid_ring.Ncring]
pow_pos_comm [in Coq.setoid_ring.Ncring]
pow_pos_strict [in Coq.micromega.ZifyInst]
pow_sqr [in Coq.Reals.Cos_rel]
pow1 [in Coq.Reals.Rfunctions]
pow2_sqrt [in Coq.Reals.R_sqrt]
pow2_nz [in Coq.Numbers.Cyclic.Int63.Int63]
pow2_pos [in Coq.Numbers.Cyclic.Int63.Int63]
pow2_abs [in Coq.Reals.Ratan]
pow2_ge_0 [in Coq.Reals.Ratan]
Pphi_dev_ok [in Coq.setoid_ring.Ring_polynom]
Pphi_pow_ok [in Coq.setoid_ring.Ring_polynom]
Pphi_avoid_ok [in Coq.setoid_ring.Ring_polynom]
Pphi0 [in Coq.setoid_ring.Ring_polynom]
Pphi0 [in Coq.micromega.EnvRing]
Pphi0 [in Coq.setoid_ring.Ncring_polynom]
Pphi1 [in Coq.setoid_ring.Ring_polynom]
Pphi1 [in Coq.micromega.EnvRing]
Pphi1 [in Coq.setoid_ring.Ncring_polynom]
Pplus_minus [in Coq.PArith.BinPos]
Pplus_one_succ_l [in Coq.PArith.BinPos]
Pplus_one_succ_r [in Coq.PArith.BinPos]
Ppow_N_ok [in Coq.setoid_ring.Ring_polynom]
Ppow_pos_ok [in Coq.setoid_ring.Ring_polynom]
Ppow_N_ok [in Coq.micromega.EnvRing]
Ppow_pos_ok [in Coq.micromega.EnvRing]
Ppow_N_ok [in Coq.setoid_ring.Ncring_polynom]
Ppow_pos_ok [in Coq.setoid_ring.Ncring_polynom]
Ppred_minus [in Coq.PArith.BinPos]
predc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
PredExt_imp_PropFunExt [in Coq.Logic.PropExtensionalityFacts]
PredExt_imp_PropExt [in Coq.Logic.PropExtensionalityFacts]
predicate_implication_pointwise [in Coq.Classes.Morphisms_Relations]
predicate_equivalence_pointwise [in Coq.Classes.Morphisms_Relations]
pred_of_minus [in Coq.Arith.Minus]
pred_Sn [in Coq.Init.Peano]
pred_spec [in Coq.Numbers.Cyclic.Int63.Int63]
pred_ext_and_rel_choice_imp_EM [in Coq.Logic.Diaconescu]
prefix_correct [in Coq.Strings.String]
PreWeakKonigsLemma [in Coq.Logic.WKL]
pre_cos_bound [in Coq.Reals.Rtrigo_alt]
pre_sin_bound [in Coq.Reals.Rtrigo_alt]
prime_power_prime [in Coq.ZArith.Zpow_facts]
prime_div_prime [in Coq.ZArith.Znumtheory]
prime_alt [in Coq.ZArith.Znumtheory]
prime_ge_2 [in Coq.ZArith.Znumtheory]
prime_3 [in Coq.ZArith.Znumtheory]
prime_2 [in Coq.ZArith.Znumtheory]
prime_mult [in Coq.ZArith.Znumtheory]
prime_rel_prime [in Coq.ZArith.Znumtheory]
prime_divisors [in Coq.ZArith.Znumtheory]
Prim2SF_inj [in Coq.Floats.FloatAxioms]
prod_length [in Coq.Lists.List]
prod_SO_Rle [in Coq.Reals.Rprod]
prod_SO_pos [in Coq.Reals.Rprod]
prod_SO_split [in Coq.Reals.Rprod]
prod_curry_uncurry [in Coq.Program.Combinators]
prod_uncurry_curry [in Coq.Program.Combinators]
project [in Coq.rtauto.Rtauto]
project_In [in Coq.rtauto.Rtauto]
projT1_injective [in Coq.Logic.Diaconescu]
proj1 [in Coq.Init.Logic]
proj2 [in Coq.Init.Logic]
prolongement_C0 [in Coq.Reals.Rtopology]
ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq [in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subsetT_eq_compat [in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subset_eq_compat [in Coq.Logic.ProofIrrelevanceFacts]
proof_irrelevance [in Coq.Logic.PropExtensionality]
proof_irrelevance [in Coq.Logic.Classical_Prop]
proof_irrel_rel_choice_imp_eq_dec' [in Coq.Logic.Diaconescu]
proof_irrel_rel_choice_imp_eq_dec [in Coq.Logic.Diaconescu]
proof_irrel [in Coq.Logic.Diaconescu]
proof_irrelevance_cci [in Coq.Logic.ClassicalFacts]
proof_irrelevance_cc [in Coq.Logic.ClassicalFacts]
proper_sym_impl_iff_2 [in Coq.Classes.Morphisms]
proper_sym_impl_iff [in Coq.Classes.Morphisms]
proper_sym_flip_2 [in Coq.Classes.Morphisms]
proper_sym_flip [in Coq.Classes.Morphisms]
proper_normalizes_proper [in Coq.Classes.Morphisms]
proper_eq [in Coq.Classes.Morphisms]
proper_proper_proxy [in Coq.Classes.Morphisms]
proper_sym_arrow_iffT_2 [in Coq.Classes.CMorphisms]
proper_sym_impl_iff_2 [in Coq.Classes.CMorphisms]
proper_sym_arrow_iffT [in Coq.Classes.CMorphisms]
proper_sym_impl_iff [in Coq.Classes.CMorphisms]
proper_sym_flip_2 [in Coq.Classes.CMorphisms]
proper_sym_flip [in Coq.Classes.CMorphisms]
proper_normalizes_proper [in Coq.Classes.CMorphisms]
proper_eq [in Coq.Classes.CMorphisms]
proper_proper_proxy [in Coq.Classes.CMorphisms]
PropExt_imp_RefutPropExt [in Coq.Logic.PropExtensionalityFacts]
PropExt_imp_ProvPropExt [in Coq.Logic.PropExtensionalityFacts]
PropExt_and_PropFunExt_iff_PredExt [in Coq.Logic.PropExtensionalityFacts]
PropExt_and_PropFunExt_imp_PredExt [in Coq.Logic.PropExtensionalityFacts]
PropNeqType.paradox [in Coq.Logic.Hurkens]
Props.choose_spec3 [in Coq.MSets.MSetGenTree]
Props.choose_spec2 [in Coq.MSets.MSetGenTree]
Props.choose_spec1 [in Coq.MSets.MSetGenTree]
Props.compare_spec [in Coq.MSets.MSetGenTree]
Props.compare_Cmp [in Coq.MSets.MSetGenTree]
Props.compare_cont_Cmp [in Coq.MSets.MSetGenTree]
Props.compare_more_Cmp [in Coq.MSets.MSetGenTree]
Props.compare_end_Cmp [in Coq.MSets.MSetGenTree]
Props.cons_1 [in Coq.MSets.MSetGenTree]
Props.elements_sort_ok [in Coq.MSets.MSetGenTree]
Props.elements_node [in Coq.MSets.MSetGenTree]
Props.elements_app [in Coq.MSets.MSetGenTree]
Props.elements_cardinal [in Coq.MSets.MSetGenTree]
Props.elements_aux_cardinal [in Coq.MSets.MSetGenTree]
Props.elements_spec2w [in Coq.MSets.MSetGenTree]
Props.elements_spec2 [in Coq.MSets.MSetGenTree]
Props.elements_spec2' [in Coq.MSets.MSetGenTree]
Props.elements_spec1 [in Coq.MSets.MSetGenTree]
Props.elements_spec1' [in Coq.MSets.MSetGenTree]
Props.empty_spec [in Coq.MSets.MSetGenTree]
Props.equal_spec [in Coq.MSets.MSetGenTree]
Props.eq_Leq [in Coq.MSets.MSetGenTree]
Props.exists_spec [in Coq.MSets.MSetGenTree]
Props.flatten_e_elements [in Coq.MSets.MSetGenTree]
Props.fold_spec [in Coq.MSets.MSetGenTree]
Props.fold_spec' [in Coq.MSets.MSetGenTree]
Props.for_all_spec [in Coq.MSets.MSetGenTree]
Props.gtb_tree_iff [in Coq.MSets.MSetGenTree]
Props.gt_tree_trans [in Coq.MSets.MSetGenTree]
Props.gt_tree_not_in [in Coq.MSets.MSetGenTree]
Props.gt_tree_node [in Coq.MSets.MSetGenTree]
Props.gt_leaf [in Coq.MSets.MSetGenTree]
Props.In_leaf_iff [in Coq.MSets.MSetGenTree]
Props.In_node_iff [in Coq.MSets.MSetGenTree]
Props.In_1 [in Coq.MSets.MSetGenTree]
Props.isok_iff [in Coq.MSets.MSetGenTree]
Props.is_empty_spec [in Coq.MSets.MSetGenTree]
Props.ltb_tree_iff [in Coq.MSets.MSetGenTree]
Props.lt_tree_trans [in Coq.MSets.MSetGenTree]
Props.lt_tree_not_in [in Coq.MSets.MSetGenTree]
Props.lt_tree_node [in Coq.MSets.MSetGenTree]
Props.lt_leaf [in Coq.MSets.MSetGenTree]
Props.maxdepth_log_cardinal [in Coq.MSets.MSetGenTree]
Props.maxdepth_cardinal [in Coq.MSets.MSetGenTree]
Props.max_elt_spec3 [in Coq.MSets.MSetGenTree]
Props.max_elt_spec2 [in Coq.MSets.MSetGenTree]
Props.max_elt_spec1 [in Coq.MSets.MSetGenTree]
Props.mem_spec [in Coq.MSets.MSetGenTree]
Props.mindepth_log_cardinal [in Coq.MSets.MSetGenTree]
Props.mindepth_cardinal [in Coq.MSets.MSetGenTree]
Props.mindepth_maxdepth [in Coq.MSets.MSetGenTree]
Props.min_elt_spec3 [in Coq.MSets.MSetGenTree]
Props.min_elt_spec2 [in Coq.MSets.MSetGenTree]
Props.min_elt_spec1 [in Coq.MSets.MSetGenTree]
Props.rev_elements_rev [in Coq.MSets.MSetGenTree]
Props.rev_elements_node [in Coq.MSets.MSetGenTree]
Props.rev_elements_app [in Coq.MSets.MSetGenTree]
Props.sorted_app_inv [in Coq.MSets.MSetGenTree]
Props.subsetl_spec [in Coq.MSets.MSetGenTree]
Props.subsetr_spec [in Coq.MSets.MSetGenTree]
Props.subset_spec [in Coq.MSets.MSetGenTree]
prop_congr [in Coq.ssr.ssrbool]
prop_eps [in Coq.Reals.Rlimit]
prop_ext [in Coq.Logic.Diaconescu]
prop_ext_retract_A_A_imp_A [in Coq.Logic.ClassicalFacts]
prop_ext_A_eq_A_imp_A [in Coq.Logic.ClassicalFacts]
prop_ext_em_degen [in Coq.Logic.ClassicalFacts]
prop_degen_em [in Coq.Logic.ClassicalFacts]
prop_degen_ext [in Coq.Logic.ClassicalFacts]
provable_prop_ext [in Coq.Logic.ClassicalFacts]
pr_nu_xeq [in Coq.Reals.Ranalysis1]
pr_nu [in Coq.Reals.Ranalysis1]
pr_nu_var2 [in Coq.Reals.Ranalysis4]
pr_nu_var [in Coq.Reals.Ranalysis4]
pr_nu_var2_interv [in Coq.Reals.Ranalysis5]
Pshiftl_nat_plus [in Coq.NArith.Ndigits]
Pshiftl_nat_N [in Coq.NArith.Ndigits]
Pshiftl_nat_S [in Coq.NArith.Ndigits]
Pshiftl_nat_0 [in Coq.NArith.Ndigits]
psos_r1 [in Coq.nsatz.NsatzTactic]
psos_r1b [in Coq.nsatz.NsatzTactic]
Psquare_ok [in Coq.micromega.EnvRing]
Psquare_ok [in Coq.setoid_ring.Ncring_polynom]
PsubC_ok [in Coq.setoid_ring.Ring_polynom]
PsubC_ok [in Coq.micromega.EnvRing]
PSubstL_ok [in Coq.setoid_ring.Ring_polynom]
PSubstL_ok [in Coq.micromega.EnvRing]
PSubstL1_ok [in Coq.setoid_ring.Ring_polynom]
PSubstL1_ok [in Coq.micromega.EnvRing]
PsubX_ok [in Coq.micromega.EnvRing]
Psub_ok [in Coq.setoid_ring.Ring_polynom]
Psub_opp [in Coq.setoid_ring.Ring_polynom]
Psub_ok [in Coq.micromega.EnvRing]
Psub_ok [in Coq.setoid_ring.Ncring_polynom]
Psucc_Gt [in Coq.rtauto.Bintree]
ps_atan_continuity_pt_1 [in Coq.Reals.Ratan]
ps_atanSeq_continuity_pt_1 [in Coq.Reals.Ratan]
ps_atan_opp [in Coq.Reals.Ratan]
ps_atan_exists_1_opp [in Coq.Reals.Ratan]
ps_atan0_0 [in Coq.Reals.Ratan]
Ptail_bounded [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Ptail_pos [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Ptestbit_Pbit [in Coq.NArith.Ndigits]
push_not_empty [in Coq.rtauto.Bintree]
Pxor_semantics [in Coq.NArith.Ndigits]
P_eventually_implies_acc_ex [in Coq.Logic.ConstructiveEpsilon]
P_eventually_implies_acc [in Coq.Logic.ConstructiveEpsilon]
P_implies_acc [in Coq.Logic.ConstructiveEpsilon]
P_Rmin [in Coq.Reals.Rpower]
P'_decidable [in Coq.Logic.ConstructiveEpsilon]
P0Z_correct [in Coq.nsatz.NsatzTactic]
p2ibis_spec [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2ibis_bounded [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2i_p2ibis [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2p1 [in Coq.Logic.ClassicalFacts]
p2p2 [in Coq.Logic.ClassicalFacts]
| 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 | (70451 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |