| 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 | (26071 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) |
| 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (508 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 | (308 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 | (479 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 | (496 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 | (906 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 | (1204 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 | (4844 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 | (166 entries) |
S (lemma)
sameP [in Stdlib.ssr.ssrbool]same_genZ [in Stdlib.setoid_ring.Ncring_initial]
same_gen [in Stdlib.setoid_ring.Ncring_initial]
same_genN [in Stdlib.setoid_ring.InitialRing]
same_genZ [in Stdlib.setoid_ring.InitialRing]
same_gen [in Stdlib.setoid_ring.InitialRing]
same_relation_is_equivalence [in Stdlib.Sets.Relations_1_facts]
scal_sum [in Stdlib.Reals.PartSum]
selectOneInSum [in Stdlib.Reals.Abstract.ConstructiveSum]
Seminus_Empty_set_r [in Stdlib.Sets.Powerset_facts]
Seminus_Empty_set_l [in Stdlib.Sets.Powerset_facts]
seq_cv_proper [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
seq_S [in Stdlib.Lists.List]
seq_app [in Stdlib.Lists.List]
seq_NoDup [in Stdlib.Lists.List]
seq_shift [in Stdlib.Lists.List]
seq_nth [in Stdlib.Lists.List]
seq_congr [in Stdlib.Sets.Uniset]
seq_right [in Stdlib.Sets.Uniset]
seq_left [in Stdlib.Sets.Uniset]
seq_sym [in Stdlib.Sets.Uniset]
seq_trans [in Stdlib.Sets.Uniset]
seq_refl [in Stdlib.Sets.Uniset]
series_cv_shift' [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_shift [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_triangle [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_abs_remainder [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_remainder_maj [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_eq [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_nonneg [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_minus [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_plus [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_scale [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_opp [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_abs_cv [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_abs_eq [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_unique [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_abs_lt [in Stdlib.Reals.Abstract.ConstructiveSum]
series_cv_maj [in Stdlib.Reals.Abstract.ConstructiveSum]
setcover_intro [in Stdlib.Sets.Powerset_facts]
setcover_inv [in Stdlib.Sets.Powerset_Classical_facts]
Setminus_Included_empty [in Stdlib.Sets.Powerset_facts]
Setminus_Disjoint_noop [in Stdlib.Sets.Powerset_facts]
Setminus_Union_r [in Stdlib.Sets.Powerset_facts]
Setminus_Union_l [in Stdlib.Sets.Powerset_facts]
Setminus_intro [in Stdlib.Sets.Constructive_sets]
setoid_trans [in Stdlib.Classes.SetoidClass]
setoid_sym [in Stdlib.Classes.SetoidClass]
setoid_refl [in Stdlib.Classes.SetoidClass]
setoid_functional_choice_second_characterization [in Stdlib.Logic.ChoiceFacts]
setoid_functional_choice_first_characterization [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_imp_repr_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_imp_functional_rel_reification [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_imp_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_iff_simple_setoid_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_imp_simple_setoid_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_iff_gen_setoid_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_fun_choice_imp_gen_setoid_fun_choice [in Stdlib.Logic.ChoiceFacts]
setoid_choice [in Stdlib.Logic.SetoidChoice]
set_diff_trivial [in Stdlib.Lists.ListSet]
set_diff_nodup [in Stdlib.Lists.ListSet]
set_diff_iff [in Stdlib.Lists.ListSet]
set_diff_elim2 [in Stdlib.Lists.ListSet]
set_diff_elim1 [in Stdlib.Lists.ListSet]
set_diff_intro [in Stdlib.Lists.ListSet]
set_inter_nodup [in Stdlib.Lists.ListSet]
set_inter_iff [in Stdlib.Lists.ListSet]
set_inter_elim [in Stdlib.Lists.ListSet]
set_inter_elim2 [in Stdlib.Lists.ListSet]
set_inter_elim1 [in Stdlib.Lists.ListSet]
set_inter_intro [in Stdlib.Lists.ListSet]
set_union_emptyR [in Stdlib.Lists.ListSet]
set_union_emptyL [in Stdlib.Lists.ListSet]
set_union_nodup [in Stdlib.Lists.ListSet]
set_union_iff [in Stdlib.Lists.ListSet]
set_union_elim [in Stdlib.Lists.ListSet]
set_union_intro [in Stdlib.Lists.ListSet]
set_union_intro2 [in Stdlib.Lists.ListSet]
set_union_intro1 [in Stdlib.Lists.ListSet]
set_remove_nodup [in Stdlib.Lists.ListSet]
set_remove_iff [in Stdlib.Lists.ListSet]
set_remove_3 [in Stdlib.Lists.ListSet]
set_remove_2 [in Stdlib.Lists.ListSet]
set_remove_1 [in Stdlib.Lists.ListSet]
set_add_nodup [in Stdlib.Lists.ListSet]
set_add_iff [in Stdlib.Lists.ListSet]
set_add_not_empty [in Stdlib.Lists.ListSet]
set_add_elim2 [in Stdlib.Lists.ListSet]
set_add_elim [in Stdlib.Lists.ListSet]
set_add_intro [in Stdlib.Lists.ListSet]
set_add_intro2 [in Stdlib.Lists.ListSet]
set_add_intro1 [in Stdlib.Lists.ListSet]
set_mem_complete2 [in Stdlib.Lists.ListSet]
set_mem_complete1 [in Stdlib.Lists.ListSet]
set_mem_correct2 [in Stdlib.Lists.ListSet]
set_mem_correct1 [in Stdlib.Lists.ListSet]
set_mem_ind2 [in Stdlib.Lists.ListSet]
set_mem_ind [in Stdlib.Lists.ListSet]
set_In_dec [in Stdlib.Lists.ListSet]
SFL_continuity [in Stdlib.Reals.PSeries_reg]
SFL_continuity_pt [in Stdlib.Reals.PSeries_reg]
SF2Prim_inj [in Stdlib.Floats.FloatAxioms]
shiftin_last [in Stdlib.Vectors.VectorSpec]
shiftin_nth [in Stdlib.Vectors.VectorSpec]
shiftrepeat_last [in Stdlib.Vectors.VectorSpec]
shiftrepeat_nth [in Stdlib.Vectors.VectorSpec]
shift_pos_correct [in Stdlib.ZArith.Zpower]
shift_pos_nat [in Stdlib.ZArith.Zpower]
shift_nat_correct [in Stdlib.ZArith.Zpower]
shift_nat_plus [in Stdlib.ZArith.Zpower]
shift_equiv [in Stdlib.ZArith.Zpower]
shift_pos_equiv [in Stdlib.ZArith.Zpower]
shift_nat_equiv [in Stdlib.ZArith.Zpower]
shift_unshift_mod_3 [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
shift_unshift_mod_2 [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
shift_value [in Stdlib.Floats.FloatLemmas]
sigma_eq_arg [in Stdlib.Reals.Rsigma]
sigma_last [in Stdlib.Reals.Rsigma]
sigma_first [in Stdlib.Reals.Rsigma]
sigma_diff_neg [in Stdlib.Reals.Rsigma]
sigma_diff [in Stdlib.Reals.Rsigma]
sigma_split [in Stdlib.Reals.Rsigma]
Signed.of_inj_pos [in Stdlib.Numbers.HexadecimalPos]
Signed.of_int_norm [in Stdlib.Numbers.HexadecimalPos]
Signed.of_to [in Stdlib.Numbers.HexadecimalPos]
Signed.of_inj_pos [in Stdlib.Numbers.DecimalN]
Signed.of_int_norm [in Stdlib.Numbers.DecimalN]
Signed.of_to [in Stdlib.Numbers.DecimalN]
Signed.of_inj_pos [in Stdlib.Numbers.DecimalNat]
Signed.of_int_norm [in Stdlib.Numbers.DecimalNat]
Signed.of_to [in Stdlib.Numbers.DecimalNat]
Signed.of_inj_pos [in Stdlib.Numbers.HexadecimalNat]
Signed.of_int_norm [in Stdlib.Numbers.HexadecimalNat]
Signed.of_to [in Stdlib.Numbers.HexadecimalNat]
Signed.of_inj_pos [in Stdlib.Numbers.DecimalPos]
Signed.of_int_norm [in Stdlib.Numbers.DecimalPos]
Signed.of_to [in Stdlib.Numbers.DecimalPos]
Signed.of_inj_pos [in Stdlib.Numbers.HexadecimalN]
Signed.of_int_norm [in Stdlib.Numbers.HexadecimalN]
Signed.of_to [in Stdlib.Numbers.HexadecimalN]
Signed.to_int_pos_surj [in Stdlib.Numbers.HexadecimalPos]
Signed.to_int_inj [in Stdlib.Numbers.HexadecimalPos]
Signed.to_of [in Stdlib.Numbers.HexadecimalPos]
Signed.to_int_pos_surj [in Stdlib.Numbers.DecimalN]
Signed.to_int_inj [in Stdlib.Numbers.DecimalN]
Signed.to_of [in Stdlib.Numbers.DecimalN]
Signed.to_int_pos_surj [in Stdlib.Numbers.DecimalNat]
Signed.to_int_inj [in Stdlib.Numbers.DecimalNat]
Signed.to_of [in Stdlib.Numbers.DecimalNat]
Signed.to_int_pos_surj [in Stdlib.Numbers.HexadecimalNat]
Signed.to_int_inj [in Stdlib.Numbers.HexadecimalNat]
Signed.to_of [in Stdlib.Numbers.HexadecimalNat]
Signed.to_int_pos_surj [in Stdlib.Numbers.DecimalPos]
Signed.to_int_inj [in Stdlib.Numbers.DecimalPos]
Signed.to_of [in Stdlib.Numbers.DecimalPos]
Signed.to_int_pos_surj [in Stdlib.Numbers.HexadecimalN]
Signed.to_int_inj [in Stdlib.Numbers.HexadecimalN]
Signed.to_of [in Stdlib.Numbers.HexadecimalN]
sigT_prod_sigT [in Stdlib.Init.Specif]
sig_not_dec [in Stdlib.Reals.Rlogic]
sig_forall_dec [in Stdlib.Reals.Rlogic]
sig_lub [in Stdlib.Reals.Abstract.ConstructiveLUB]
simple_setoid_fun_choice_imp_setoid_fun_choice [in Stdlib.Logic.ChoiceFacts]
simplification_K [in Stdlib.Program.Equality]
simplification_existT1 [in Stdlib.Program.Equality]
simplification_existT2 [in Stdlib.Program.Equality]
simplification_heq [in Stdlib.Program.Equality]
Simplify_add [in Stdlib.Sets.Powerset_Classical_facts]
simpl_predE [in Stdlib.ssr.ssrbool]
simpl_sin_n [in Stdlib.Reals.Rtrigo_def]
simpl_cos_n [in Stdlib.Reals.Rtrigo_def]
simpl_fact [in Stdlib.Reals.Rfunctions]
SIN [in Stdlib.Reals.Rtrigo1]
sincl_add_x [in Stdlib.Sets.Powerset_Classical_facts]
Singleton_is_finite [in Stdlib.Sets.Finite_sets_facts]
Singleton_atomic [in Stdlib.Sets.Powerset_Classical_facts]
Singleton_intro [in Stdlib.Sets.Constructive_sets]
Singleton_inv [in Stdlib.Sets.Constructive_sets]
singleton_choice [in Stdlib.Logic.ClassicalChoice]
single_z_r_R1_depr [in Stdlib.Reals.RIneq]
single_limit [in Stdlib.Reals.Rlimit]
singlx [in Stdlib.Sets.Powerset_facts]
sinh_0 [in Stdlib.Reals.Rtrigo_def]
sinh_arcsinh [in Stdlib.Reals.Rpower]
sinh_lt [in Stdlib.Reals.Ranalysis4]
sin_pi_plus [in Stdlib.Reals.Rtrigo_facts]
sin_pi_minus [in Stdlib.Reals.Rtrigo_facts]
sin_tan [in Stdlib.Reals.Rtrigo_facts]
sin_cos_Rabs [in Stdlib.Reals.Rtrigo_facts]
sin_cos_opp [in Stdlib.Reals.Rtrigo_facts]
sin_cos [in Stdlib.Reals.Rtrigo_facts]
sin_0 [in Stdlib.Reals.Rtrigo_def]
sin_antisym [in Stdlib.Reals.Rtrigo_def]
sin_no_R0 [in Stdlib.Reals.Rtrigo_def]
sin_gt_x [in Stdlib.Reals.Ratan]
sin_acos [in Stdlib.Reals.Ratan]
sin_asin [in Stdlib.Reals.Ratan]
sin_atan [in Stdlib.Reals.Ratan]
sin_lt_x [in Stdlib.Reals.Ratan]
sin_lb_ge_0 [in Stdlib.Reals.Rtrigo_calc]
sin_cos5PI4 [in Stdlib.Reals.Rtrigo_calc]
sin_5PI4 [in Stdlib.Reals.Rtrigo_calc]
sin_2PI3 [in Stdlib.Reals.Rtrigo_calc]
sin_PI3 [in Stdlib.Reals.Rtrigo_calc]
sin_3PI4 [in Stdlib.Reals.Rtrigo_calc]
sin_PI4 [in Stdlib.Reals.Rtrigo_calc]
sin_PI6 [in Stdlib.Reals.Rtrigo_calc]
sin_PI6_cos_PI3 [in Stdlib.Reals.Rtrigo_calc]
sin_PI3_cos_PI6 [in Stdlib.Reals.Rtrigo_calc]
sin_cos_PI4 [in Stdlib.Reals.Rtrigo_calc]
sin_3PI2 [in Stdlib.Reals.Rtrigo_calc]
sin_eq_O_2PI_1 [in Stdlib.Reals.Rtrigo1]
sin_eq_O_2PI_0 [in Stdlib.Reals.Rtrigo1]
sin_eq_0_0 [in Stdlib.Reals.Rtrigo1]
sin_eq_0_1 [in Stdlib.Reals.Rtrigo1]
sin_decr_1 [in Stdlib.Reals.Rtrigo1]
sin_decr_0 [in Stdlib.Reals.Rtrigo1]
sin_incr_1 [in Stdlib.Reals.Rtrigo1]
sin_incr_0 [in Stdlib.Reals.Rtrigo1]
sin_inj [in Stdlib.Reals.Rtrigo1]
sin_decreasing_1 [in Stdlib.Reals.Rtrigo1]
sin_decreasing_0 [in Stdlib.Reals.Rtrigo1]
sin_increasing_1 [in Stdlib.Reals.Rtrigo1]
sin_increasing_0 [in Stdlib.Reals.Rtrigo1]
sin_lt_0_var [in Stdlib.Reals.Rtrigo1]
sin_lt_0 [in Stdlib.Reals.Rtrigo1]
sin_le_0 [in Stdlib.Reals.Rtrigo1]
sin_ge_0 [in Stdlib.Reals.Rtrigo1]
sin_gt_0 [in Stdlib.Reals.Rtrigo1]
sin_lb_gt_0 [in Stdlib.Reals.Rtrigo1]
SIN_bound [in Stdlib.Reals.Rtrigo1]
sin_shift [in Stdlib.Reals.Rtrigo1]
sin_period [in Stdlib.Reals.Rtrigo1]
sin_PI_x [in Stdlib.Reals.Rtrigo1]
sin_2PI [in Stdlib.Reals.Rtrigo1]
sin_neg [in Stdlib.Reals.Rtrigo1]
sin_2a [in Stdlib.Reals.Rtrigo1]
sin_minus [in Stdlib.Reals.Rtrigo1]
sin_plus [in Stdlib.Reals.Rtrigo1]
sin_cos [in Stdlib.Reals.Rtrigo1]
sin_bound [in Stdlib.Reals.Rtrigo1]
sin_PI [in Stdlib.Reals.Rtrigo1]
sin_PI2 [in Stdlib.Reals.Rtrigo1]
sin_pos_tech [in Stdlib.Reals.Rtrigo1]
sin_gt_cos_7_8 [in Stdlib.Reals.Rtrigo1]
sin2 [in Stdlib.Reals.Rtrigo1]
sin2_bound [in Stdlib.Reals.Rtrigo_facts]
sin2_cos2 [in Stdlib.Reals.Rtrigo1]
skipn_seq [in Stdlib.Lists.List]
skipn_map [in Stdlib.Lists.List]
skipn_rev [in Stdlib.Lists.List]
skipn_app [in Stdlib.Lists.List]
skipn_skipn [in Stdlib.Lists.List]
skipn_all_iff [in Stdlib.Lists.List]
skipn_all2 [in Stdlib.Lists.List]
skipn_all [in Stdlib.Lists.List]
skipn_cons [in Stdlib.Lists.List]
skipn_nil [in Stdlib.Lists.List]
skipn_0 [in Stdlib.Lists.List]
skipn_firstn_comm [in Stdlib.Lists.List]
slexprod_lexprod [in Stdlib.Relations.Relation_Operators]
SlowMorph_increasing [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph_increasing_Ql [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph_increasing_Qr [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
small_drinkers'_paradox [in Stdlib.Logic.Epsilon]
Smorph_morph [in Stdlib.setoid_ring.Ring_theory]
Smorph_sub [in Stdlib.setoid_ring.Ring_theory]
Smorph_opp [in Stdlib.setoid_ring.Ring_theory]
SndRel_ProdRel [in Stdlib.Classes.RelationPairs]
snd_list_prod [in Stdlib.Lists.List]
solution_right [in Stdlib.Program.Equality]
solution_left [in Stdlib.Program.Equality]
Some_inj [in Stdlib.ssr.ssrfun]
SortA_equivlistA_eqlistA [in Stdlib.Lists.SetoidList]
SortA_NoDupA [in Stdlib.Lists.SetoidList]
SortA_app [in Stdlib.Lists.SetoidList]
SortA_InfA_InA [in Stdlib.Lists.SetoidList]
Sorted_StronglySorted [in Stdlib.Sorting.Sorted]
Sorted_extends [in Stdlib.Sorting.Sorted]
Sorted_LocallySorted_iff [in Stdlib.Sorting.Sorted]
Sorted_rect [in Stdlib.Sorting.Sorted]
Sorted_inv [in Stdlib.Sorting.Sorted]
Sort.LocallySorted_sort [in Stdlib.Sorting.Mergesort]
Sort.Permuted_sort [in Stdlib.Sorting.Mergesort]
Sort.Permuted_iter_merge [in Stdlib.Sorting.Mergesort]
Sort.Permuted_merge_stack [in Stdlib.Sorting.Mergesort]
Sort.Permuted_merge_list_to_stack [in Stdlib.Sorting.Mergesort]
Sort.Permuted_merge [in Stdlib.Sorting.Mergesort]
Sort.Sorted_sort [in Stdlib.Sorting.Mergesort]
Sort.Sorted_iter_merge [in Stdlib.Sorting.Mergesort]
Sort.Sorted_merge_stack [in Stdlib.Sorting.Mergesort]
Sort.Sorted_merge_list_to_stack [in Stdlib.Sorting.Mergesort]
Sort.Sorted_merge [in Stdlib.Sorting.Mergesort]
Sort.StronglySorted_sort [in Stdlib.Sorting.Mergesort]
splitat_append [in Stdlib.Vectors.VectorSpec]
splitSum [in Stdlib.Reals.Abstract.ConstructiveSum]
split_lt_succ [in Stdlib.Reals.Runcountable]
split_couple_eq [in Stdlib.Reals.Runcountable]
split_cat_sub [in Stdlib.Strings.PString]
split_combine [in Stdlib.Lists.List]
split_nth [in Stdlib.Lists.List]
split_nz_r [in Stdlib.setoid_ring.Field_theory]
split_nz_l [in Stdlib.setoid_ring.Field_theory]
split_ok_r [in Stdlib.setoid_ring.Field_theory]
split_ok_l [in Stdlib.setoid_ring.Field_theory]
split_aux_ok [in Stdlib.setoid_ring.Field_theory]
split_aux_ok1 [in Stdlib.setoid_ring.Field_theory]
Splus_lt [in Stdlib.funind.Recdef]
Spr1_inj [in Stdlib.Logic.StrictProp]
sqrt_cauchy [in Stdlib.Reals.R_sqrt]
sqrt_inv [in Stdlib.Reals.R_sqrt]
sqrt_more [in Stdlib.Reals.R_sqrt]
sqrt_less [in Stdlib.Reals.R_sqrt]
sqrt_less_alt [in Stdlib.Reals.R_sqrt]
sqrt_inj [in Stdlib.Reals.R_sqrt]
sqrt_neg_0 [in Stdlib.Reals.R_sqrt]
sqrt_le_1 [in Stdlib.Reals.R_sqrt]
sqrt_le_1_alt [in Stdlib.Reals.R_sqrt]
sqrt_le_0 [in Stdlib.Reals.R_sqrt]
sqrt_lt_1 [in Stdlib.Reals.R_sqrt]
sqrt_lt_1_alt [in Stdlib.Reals.R_sqrt]
sqrt_lt_0 [in Stdlib.Reals.R_sqrt]
sqrt_lt_0_alt [in Stdlib.Reals.R_sqrt]
sqrt_div [in Stdlib.Reals.R_sqrt]
sqrt_div_alt [in Stdlib.Reals.R_sqrt]
sqrt_lt_R0 [in Stdlib.Reals.R_sqrt]
sqrt_mult [in Stdlib.Reals.R_sqrt]
sqrt_mult_alt [in Stdlib.Reals.R_sqrt]
sqrt_Rsqr_abs [in Stdlib.Reals.R_sqrt]
sqrt_pow2 [in Stdlib.Reals.R_sqrt]
sqrt_Rsqr [in Stdlib.Reals.R_sqrt]
sqrt_square [in Stdlib.Reals.R_sqrt]
sqrt_def [in Stdlib.Reals.R_sqrt]
sqrt_lem_1 [in Stdlib.Reals.R_sqrt]
sqrt_lem_0 [in Stdlib.Reals.R_sqrt]
sqrt_eq_0 [in Stdlib.Reals.R_sqrt]
sqrt_1 [in Stdlib.Reals.R_sqrt]
sqrt_0 [in Stdlib.Reals.R_sqrt]
sqrt_sqrt [in Stdlib.Reals.R_sqrt]
sqrt_positivity [in Stdlib.Reals.R_sqrt]
sqrt_pos [in Stdlib.Reals.R_sqrt]
sqrt_continuity_pt [in Stdlib.Reals.Sqrt_reg]
sqrt_continuity_pt_R1 [in Stdlib.Reals.Sqrt_reg]
sqrt_var_maj [in Stdlib.Reals.Sqrt_reg]
sqrt_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_init [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_step_correct [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_test_true [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_test_false [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_main [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt_main_trick [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt2_neq_0 [in Stdlib.Reals.Rtrigo_calc]
sqrt2_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt2_step_correct [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt2_lower_bound [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt2_step_def [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sqrt3_2_neq_0 [in Stdlib.Reals.Rtrigo_calc]
sqr_pos [in Stdlib.ZArith.Zcomplements]
squarec_spec [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
square_not_prime [in Stdlib.ZArith.Znumtheory]
SReqe_Reqe [in Stdlib.setoid_ring.Ring_theory]
SRmorph_Rmorph [in Stdlib.setoid_ring.Ring_theory]
SRopp_add [in Stdlib.setoid_ring.Ring_theory]
SRopp_mul_l [in Stdlib.setoid_ring.Ring_theory]
SRopp_ext [in Stdlib.setoid_ring.Ring_theory]
SRsub_def [in Stdlib.setoid_ring.Ring_theory]
SRth_ARth [in Stdlib.setoid_ring.Ring_theory]
SSplus_lt [in Stdlib.funind.Recdef]
ssr_congr_arrow [in Stdlib.ssr.ssreflect]
ssr_have_upoly [in Stdlib.ssr.ssreflect]
ssr_have [in Stdlib.ssr.ssreflect]
Sstar_contains_Rstar [in Stdlib.Sets.Relations_2_facts]
star_monotone [in Stdlib.Sets.Relations_2_facts]
StepFun_P46 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P45 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P44 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P43 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P42 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P41 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P40 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P39 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P38 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P37 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P36 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P35 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P34 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P33 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P32 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P31 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P30 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P29 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P28 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P27 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P26 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P25 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P24 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P23 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P22 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P21 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P20 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P19 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P18 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P17 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P16 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P15 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P14 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P13 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P12 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P11 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P10 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P9 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P8 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P7 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P6 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P5 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P4 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P3 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P2 [in Stdlib.Reals.RiemannInt_SF]
StepFun_P1 [in Stdlib.Reals.RiemannInt_SF]
Streicher_K__eq_rect_eq [in Stdlib.Logic.EqdepFacts]
Streicher_K_on__eq_rect_eq_on [in Stdlib.Logic.EqdepFacts]
strictincreasing_strictdecreasing_opp [in Stdlib.Reals.MVT]
StrictOrder_PartialOrder [in Stdlib.Classes.Morphisms]
StrictOrder_PreOrder [in Stdlib.Classes.Morphisms]
StrictOrder_PartialOrder [in Stdlib.Classes.CMorphisms]
StrictOrder_PreOrder [in Stdlib.Classes.CMorphisms]
Strict_Included_inv [in Stdlib.Sets.Classical_sets]
Strict_super_set_contains_new_element [in Stdlib.Sets.Classical_sets]
Strict_inclusion_is_transitive [in Stdlib.Sets.Powerset]
Strict_inclusion_is_transitive_with_inclusion_left [in Stdlib.Sets.Powerset]
Strict_inclusion_is_transitive_with_inclusion [in Stdlib.Sets.Powerset]
Strict_Rel_is_Strict_Included [in Stdlib.Sets.Powerset]
Strict_Included_strict [in Stdlib.Sets.Constructive_sets]
Strict_Included_intro [in Stdlib.Sets.Constructive_sets]
Strict_Rel_Transitive [in Stdlib.Sets.Partial_Order]
Strict_Rel_Transitive_with_Rel_left [in Stdlib.Sets.Partial_Order]
Strict_Rel_Transitive_with_Rel [in Stdlib.Sets.Partial_Order]
string_eq_ext [in Stdlib.Strings.PString]
string_of_list_byte_of_string [in Stdlib.Strings.String]
string_of_list_ascii_of_string [in Stdlib.Strings.String]
String_as_OT.compare_spec [in Stdlib.Structures.OrdersEx]
String_as_OT.compare_helper_eq [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.compare_helper_gt [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.compare_helper_lt [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.cmp_lt [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.cmp_antisym [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.cmp_eq [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.lt_not_eq [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.lt_trans [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.lts_tail_unique [in Stdlib.Structures.OrderedTypeEx]
String_as_OT.nat_of_ascii_inverse [in Stdlib.Structures.OrderedTypeEx]
strip_commut [in Stdlib.Wellfounded.Union]
StronglySorted_Sorted [in Stdlib.Sorting.Sorted]
StronglySorted_rec [in Stdlib.Sorting.Sorted]
StronglySorted_rect [in Stdlib.Sorting.Sorted]
StronglySorted_inv [in Stdlib.Sorting.Sorted]
Strong_confluence_direct [in Stdlib.Sets.Relations_3_facts]
Strong_confluence [in Stdlib.Sets.Relations_3_facts]
Str_nth_zipWith [in Stdlib.Lists.Streams]
Str_nth_tl_zipWith [in Stdlib.Lists.Streams]
Str_nth_map [in Stdlib.Lists.Streams]
Str_nth_tl_map [in Stdlib.Lists.Streams]
Str_nth_plus [in Stdlib.Lists.Streams]
Str_nth_tl_plus [in Stdlib.Lists.Streams]
subcarryc_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
subcarry_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
subc_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
SubEqui_P9 [in Stdlib.Reals.RiemannInt]
SubEqui_P8 [in Stdlib.Reals.RiemannInt]
SubEqui_P7 [in Stdlib.Reals.RiemannInt]
SubEqui_P6 [in Stdlib.Reals.RiemannInt]
SubEqui_P5 [in Stdlib.Reals.RiemannInt]
SubEqui_P4 [in Stdlib.Reals.RiemannInt]
SubEqui_P3 [in Stdlib.Reals.RiemannInt]
SubEqui_P2 [in Stdlib.Reals.RiemannInt]
SubEqui_P1 [in Stdlib.Reals.RiemannInt]
subon_bij [in Stdlib.ssr.ssrbool]
subon1 [in Stdlib.ssr.ssrbool]
subon1l [in Stdlib.ssr.ssrbool]
subon2 [in Stdlib.ssr.ssrbool]
subrelation_symmetric [in Stdlib.Classes.RelationClasses]
subrelation_proper [in Stdlib.Classes.Morphisms]
subrelation_refl [in Stdlib.Classes.Morphisms]
subrelation_respectful [in Stdlib.Classes.Morphisms]
subrelation_proper [in Stdlib.Classes.CMorphisms]
subrelation_refl [in Stdlib.Classes.CMorphisms]
subrelation_respectful [in Stdlib.Classes.CMorphisms]
subrelation_symmetric [in Stdlib.Classes.CRelationClasses]
subrelUl [in Stdlib.ssr.ssrbool]
subrelUr [in Stdlib.ssr.ssrbool]
subset_types_imp_guarded_rel_choice_iff_rel_choice [in Stdlib.Logic.ChoiceFacts]
subset_eq [in Stdlib.Program.Subset]
substring_correct2 [in Stdlib.Strings.String]
substring_correct1 [in Stdlib.Strings.String]
Subtract_inv [in Stdlib.Sets.Classical_sets]
Subtract_intro [in Stdlib.Sets.Classical_sets]
sub_in21 [in Stdlib.ssr.ssrbool]
sub_in12 [in Stdlib.ssr.ssrbool]
sub_in3 [in Stdlib.ssr.ssrbool]
sub_in2 [in Stdlib.ssr.ssrbool]
sub_in_bij [in Stdlib.ssr.ssrbool]
sub_in111 [in Stdlib.ssr.ssrbool]
sub_in11 [in Stdlib.ssr.ssrbool]
sub_in1 [in Stdlib.ssr.ssrbool]
sub_refl [in Stdlib.ssr.ssrbool]
sub_of_Z [in Stdlib.Numbers.Cyclic.Int63.Sint63]
sub_spec [in Stdlib.Numbers.Cyclic.Int63.Sint63]
sub_sub [in Stdlib.Strings.PString]
sub_len_0 [in Stdlib.Strings.PString]
sub_full [in Stdlib.Strings.PString]
sub_get_spec [in Stdlib.Strings.PString]
sub_length_spec [in Stdlib.Strings.PString]
Sub_Add_new [in Stdlib.Sets.Powerset_Classical_facts]
succc_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
SuccNat2Pos.id_succ [in Stdlib.PArith.Pnat]
SuccNat2Pos.inj [in Stdlib.PArith.Pnat]
SuccNat2Pos.inj_compare [in Stdlib.PArith.Pnat]
SuccNat2Pos.inj_succ [in Stdlib.PArith.Pnat]
SuccNat2Pos.inj_iff [in Stdlib.PArith.Pnat]
SuccNat2Pos.inv [in Stdlib.PArith.Pnat]
SuccNat2Pos.pred_id [in Stdlib.PArith.Pnat]
succ_of_Z [in Stdlib.Numbers.Cyclic.Int63.Sint63]
succ_spec [in Stdlib.Numbers.Cyclic.Int63.Sint63]
succ_IZR [in Stdlib.Reals.RIneq]
succ_IPR [in Stdlib.Reals.RIneq]
succ_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
sumboolP [in Stdlib.ssr.ssrbool]
sum_maj1 [in Stdlib.Reals.SeqSeries]
sum_plus [in Stdlib.Reals.Cauchy_prod]
sum_N_predN [in Stdlib.Reals.Cauchy_prod]
sum_Ratan_seq_opp [in Stdlib.Reals.Ratan]
sum_inequa_Rle_lt_depr [in Stdlib.Reals.RIneq]
sum_f_R0_triangle [in Stdlib.Reals.Rfunctions]
sum_plus [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_scale [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_opp [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_Rle [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_assoc [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_const [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_eq_R0 [in Stdlib.Reals.Abstract.ConstructiveSum]
sum_cv_maj [in Stdlib.Reals.PartSum]
sum_incr [in Stdlib.Reals.PartSum]
sum_eq_R0 [in Stdlib.Reals.PartSum]
sum_growing [in Stdlib.Reals.PartSum]
sum_cte [in Stdlib.Reals.PartSum]
sum_Rle [in Stdlib.Reals.PartSum]
sum_decomposition [in Stdlib.Reals.PartSum]
sum_eq [in Stdlib.Reals.PartSum]
surjective_pairing [in Stdlib.Init.Datatypes]
Surjective_inverse [in Stdlib.Logic.FinFun]
Surjective_carac [in Stdlib.Logic.FinFun]
Surjective_list_carac [in Stdlib.Logic.FinFun]
svalP [in Stdlib.ssr.ssrfun]
swap_Acc [in Stdlib.Wellfounded.Lexicographic_Product]
symmetric_from_pre [in Stdlib.ssr.ssrbool]
symmetric_equiv_flip [in Stdlib.Classes.Morphisms]
symmetric_equiv_flip [in Stdlib.Classes.CMorphisms]
sym_EqSt [in Stdlib.Lists.Streams]
sym_right_transitive [in Stdlib.ssr.ssrbool]
sym_left_transitive [in Stdlib.ssr.ssrbool]
S_O_plus_INR_depr [in Stdlib.Reals.RIneq]
S_INR [in Stdlib.Reals.RIneq]
s2valP [in Stdlib.ssr.ssrfun]
s2valP' [in Stdlib.ssr.ssrfun]
| 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 | (26071 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) |
| 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (508 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 | (308 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 | (479 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 | (496 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 | (906 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 | (1204 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 | (4844 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 | (166 entries) |