S (lemma)
same_relation_is_equivalence [in same_relation_is_equivalence]
scal_sum [in scal_sum]
seq_nth [in seq_nth]
seq_refl [in seq_refl]
seq_right [in seq_right]
seq_left [in seq_left]
seq_congr [in seq_congr]
seq_shift [in seq_shift]
seq_sym [in seq_sym]
seq_length [in seq_length]
seq_trans [in seq_trans]
setcover_inv [in setcover_inv]
setcover_intro [in setcover_intro]
Setminus_intro [in Setminus_intro]
set_add_elim2 [in set_add_elim2]
set_union_intro1 [in set_union_intro1]
set_union_intro [in set_union_intro]
set_diff_intro [in set_diff_intro]
set_inter_elim2 [in set_inter_elim2]
set_mem_correct2 [in set_mem_correct2]
set_add_elim [in set_add_elim]
set_add_intro2 [in set_add_intro2]
set_add_intro [in set_add_intro]
set_add_intro1 [in set_add_intro1]
set_union_elim [in set_union_elim]
set_mem_ind [in set_mem_ind]
set_diff_elim2 [in set_diff_elim2]
set_In_dec [in set_In_dec]
set_mem_correct1 [in set_mem_correct1]
set_diff_trivial [in set_diff_trivial]
set_union_emptyR [in set_union_emptyR]
set_diff_elim1 [in set_diff_elim1]
set_union_emptyL [in set_union_emptyL]
set_inter_elim1 [in set_inter_elim1]
set_add_not_empty [in set_add_not_empty]
set_inter_elim [in set_inter_elim]
set_mem_complete1 [in set_mem_complete1]
set_mem_ind2 [in set_mem_ind2]
set_union_intro2 [in set_union_intro2]
set_mem_complete2 [in set_mem_complete2]
set_inter_intro [in set_inter_intro]
SFL_continuity [in SFL_continuity]
SFL_continuity_pt [in SFL_continuity_pt]
shiftin_nth [in shiftin_nth]
shiftin_last [in shiftin_last]
shiftl_spec_low [in shiftl_spec_low]
shiftl_spec_high [in shiftl_spec_high]
shiftrepeat_nth [in shiftrepeat_nth]
shiftrepeat_last [in shiftrepeat_last]
shiftr_spec [in shiftr_spec]
shift_pos_nat [in shift_pos_nat]
shift_equiv [in shift_equiv]
shift_nat_plus [in shift_nat_plus]
shift_pos_correct [in shift_pos_correct]
shift_unshift_mod [in shift_unshift_mod]
shift_nat_correct [in shift_nat_correct]
shift_unshift_mod_2 [in shift_unshift_mod_2]
shift_nat_equiv [in shift_nat_equiv]
shift_pos_equiv [in shift_pos_equiv]
sigma_split [in sigma_split]
sigma_first [in sigma_first]
sigma_eq_arg [in sigma_eq_arg]
sigma_last [in sigma_last]
sigma_diff [in sigma_diff]
sigma_diff_neg [in sigma_diff_neg]
sigT_of_sig [in sigT_of_sig]
sig_of_sigT [in sig_of_sigT]
sig_forall_dec [in sig_forall_dec]
simplification_heq [in simplification_heq]
simplification_K [in simplification_K]
simplification_existT2 [in simplification_existT2]
simplification_existT1 [in simplification_existT1]
Simplify_add [in Simplify_add]
simpl_fact [in simpl_fact]
simpl_sin_n [in simpl_sin_n]
simpl_cos_n [in simpl_cos_n]
SIN [in SIN]
sincl_add_x [in sincl_add_x]
Singleton_atomic [in Singleton_atomic]
Singleton_is_finite [in Singleton_is_finite]
singleton_choice [in singleton_choice]
Singleton_intro [in Singleton_intro]
Singleton_inv [in Singleton_inv]
single_limit [in single_limit]
single_z_r_R1 [in single_z_r_R1]
singlx [in singlx]
sinh_0 [in sinh_0]
sin_0 [in sin_0]
sin_gt_0 [in sin_gt_0]
sin_shift [in sin_shift]
sin_pos_tech [in sin_pos_tech]
sin_lb_gt_0 [in sin_lb_gt_0]
sin_decr_0 [in sin_decr_0]
sin_bound [in sin_bound]
sin_2PI3 [in sin_2PI3]
sin_no_R0 [in sin_no_R0]
sin_minus [in sin_minus]
sin_5PI4 [in sin_5PI4]
SIN_bound [in SIN_bound]
sin_eq_0_1 [in sin_eq_0_1]
sin_incr_1 [in sin_incr_1]
sin_period [in sin_period]
sin_PI_x [in sin_PI_x]
sin_decreasing_0 [in sin_decreasing_0]
sin_lt_0 [in sin_lt_0]
sin_increasing_1 [in sin_increasing_1]
sin_PI [in sin_PI]
sin_PI6 [in sin_PI6]
sin_ge_0 [in sin_ge_0]
sin_lb_ge_0 [in sin_lb_ge_0]
sin_PI4 [in sin_PI4]
sin_PI2 [in sin_PI2]
sin_cos5PI4 [in sin_cos5PI4]
sin_eq_O_2PI_1 [in sin_eq_O_2PI_1]
sin_increasing_0 [in sin_increasing_0]
sin_PI3_cos_PI6 [in sin_PI3_cos_PI6]
sin_neg [in sin_neg]
sin_PI3 [in sin_PI3]
sin_3PI2 [in sin_3PI2]
sin_lt_0_var [in sin_lt_0_var]
sin_cos [in sin_cos]
sin_PI6_cos_PI3 [in sin_PI6_cos_PI3]
sin_cos_PI4 [in sin_cos_PI4]
sin_eq_O_2PI_0 [in sin_eq_O_2PI_0]
sin_plus [in sin_plus]
sin_gt_cos_7_8 [in sin_gt_cos_7_8]
sin_le_0 [in sin_le_0]
sin_decr_1 [in sin_decr_1]
sin_2PI [in sin_2PI]
sin_2a [in sin_2a]
sin_eq_0_0 [in sin_eq_0_0]
sin_antisym [in sin_antisym]
sin_incr_0 [in sin_incr_0]
sin_decreasing_1 [in sin_decreasing_1]
sin2 [in sin2]
sin2_cos2 [in sin2_cos2]
sin3PI4 [in sin3PI4]
small_drinkers'_paradox [in small_drinkers'_paradox]
SndRel_ProdRel [in SndRel_ProdRel]
sneakl_shiftr [in sneakl_shiftr]
sneakr_shiftl [in sneakr_shiftl]
solution_right [in solution_right]
solution_left [in solution_left]
SortA_InfA_InA [in SortA_InfA_InA]
SortA_app [in SortA_app]
SortA_NoDupA [in SortA_NoDupA]
SortA_equivlistA_eqlistA [in SortA_equivlistA_eqlistA]
Sorted_rect [in Sorted_rect]
Sorted_inv [in Sorted_inv]
Sorted_extends [in Sorted_extends]
Sorted_LocallySorted_iff [in Sorted_LocallySorted_iff]
Sorted_StronglySorted [in Sorted_StronglySorted]
Sort.LocallySorted_sort [in LocallySorted_sort]
Sort.Permuted_merge_stack [in Permuted_merge_stack]
Sort.Permuted_sort [in Permuted_sort]
Sort.Permuted_iter_merge [in Permuted_iter_merge]
Sort.Permuted_merge [in Permuted_merge]
Sort.Permuted_merge_list_to_stack [in Permuted_merge_list_to_stack]
Sort.Sorted_merge [in Sorted_merge]
Sort.Sorted_merge_list_to_stack [in Sorted_merge_list_to_stack]
Sort.Sorted_sort [in Sorted_sort]
Sort.Sorted_merge_stack [in Sorted_merge_stack]
Sort.Sorted_iter_merge [in Sorted_iter_merge]
Sort.StronglySorted_sort [in StronglySorted_sort]
spec_ww_sqrt2 [in spec_ww_sqrt2]
spec_pred_c [in spec_pred_c]
spec_pred_c [in spec_pred_c]
spec_add_mul_div [in spec_add_mul_div]
spec_add_mul_div [in spec_add_mul_div]
spec_eq0 [in spec_eq0]
spec_eq0 [in spec_eq0]
spec_w_div2s [in spec_w_div2s]
spec_double_modn1_p [in spec_double_modn1_p]
spec_of_pos [in spec_of_pos]
spec_sqrt2 [in spec_sqrt2]
spec_sqrt2 [in spec_sqrt2]
spec_mul_aux [in spec_mul_aux]
spec_div21 [in spec_div21]
spec_div21 [in spec_div21]
spec_is_even [in spec_is_even]
spec_is_even [in spec_is_even]
spec_ww_opp [in spec_ww_opp]
spec_ww_head0 [in spec_ww_head0]
spec_pred [in spec_pred]
spec_pred [in spec_pred]
spec_head00 [in spec_head00]
spec_head00 [in spec_head00]
spec_double_to_Z [in spec_double_to_Z]
spec_to_N [in spec_to_N]
spec_w_div21c [in spec_w_div21c]
spec_ww_gcd [in spec_ww_gcd]
spec_double_divn1 [in spec_double_divn1]
spec_double_modn1_aux [in spec_double_modn1_aux]
spec_add [in spec_add]
spec_add [in spec_add]
spec_ww_pos_mod [in spec_ww_pos_mod]
spec_double_mul_add_n1 [in spec_double_mul_add_n1]
spec_compare_mn_1 [in spec_compare_mn_1]
spec_ww_sub [in spec_ww_sub]
spec_w_mod_gt_eq [in spec_w_mod_gt_eq]
spec_double_mul_c [in spec_double_mul_c]
spec_double_WW [in spec_double_WW]
spec_ww_add_c [in spec_ww_add_c]
spec_zdigits [in spec_zdigits]
spec_zdigits [in spec_zdigits]
spec_ww_1 [in spec_ww_1]
spec_succ_c [in spec_succ_c]
spec_succ_c [in spec_succ_c]
spec_ww_add_mul_div [in spec_ww_add_mul_div]
spec_ww_add_mul_div [in spec_ww_add_mul_div]
spec_ww_mul_c [in spec_ww_mul_c]
spec_ww_add_mul_div_aux [in spec_ww_add_mul_div_aux]
spec_ww_Bm1 [in spec_ww_Bm1]
spec_double_split [in spec_double_split]
spec_Bm1 [in spec_Bm1]
spec_ww_gcd_gt_aux_body [in spec_ww_gcd_gt_aux_body]
spec_ww_pred [in spec_ww_pred]
spec_double_modn1_0 [in spec_double_modn1_0]
spec_mul [in spec_mul]
spec_mul [in spec_mul]
spec_head0 [in spec_head0]
spec_head0 [in spec_head0]
spec_ww_square_c [in spec_ww_square_c]
spec_tail00 [in spec_tail00]
spec_tail00 [in spec_tail00]
spec_ww_mod_gt_aux [in spec_ww_mod_gt_aux]
spec_ww_sub_carry [in spec_ww_sub_carry]
spec_ww_opp_c [in spec_ww_opp_c]
spec_opp_c [in spec_opp_c]
spec_opp_c [in spec_opp_c]
spec_ww_is_even [in spec_ww_is_even]
spec_square_c [in spec_square_c]
spec_to_Z_1 [in spec_to_Z_1]
spec_square_c [in spec_square_c]
spec_ww_sqrt [in spec_ww_sqrt]
spec_sub_carry [in spec_sub_carry]
spec_sub_carry [in spec_sub_carry]
spec_ww_div [in spec_ww_div]
spec_1 [in spec_1]
spec_1 [in spec_1]
spec_ww_tail00 [in spec_ww_tail00]
spec_get_low [in spec_get_low]
spec_double_divn1_p [in spec_double_divn1_p]
spec_ww_to_Z_wBwB [in spec_ww_to_Z_wBwB]
spec_double_digits [in spec_double_digits]
spec_high [in spec_high]
spec_m1 [in spec_m1]
spec_ww_div_gt [in spec_ww_div_gt]
spec_ww_mod_gt_aux_eq [in spec_ww_mod_gt_aux_eq]
spec_tail0 [in spec_tail0]
spec_tail0 [in spec_tail0]
spec_ww_add [in spec_ww_add]
spec_ww_sub_carry_c [in spec_ww_sub_carry_c]
spec_modulo [in spec_modulo]
spec_extend [in spec_extend]
spec_compare [in spec_compare]
spec_compare [in spec_compare]
spec_ww_head1 [in spec_ww_head1]
spec_div [in spec_div]
spec_div [in spec_div]
spec_ww_compare [in spec_ww_compare]
spec_modulo_gt [in spec_modulo_gt]
spec_to_Z [in spec_to_Z]
spec_to_Z [in spec_to_Z]
spec_ww_gcd_gt [in spec_ww_gcd_gt]
spec_ww_sub_c [in spec_ww_sub_c]
spec_ww_add_carry [in spec_ww_add_carry]
spec_kara_prod [in spec_kara_prod]
spec_add_mul_divp [in spec_add_mul_divp]
spec_sub [in spec_sub]
spec_sub [in spec_sub]
spec_pos_mod [in spec_pos_mod]
spec_pos_mod [in spec_pos_mod]
spec_succ [in spec_succ]
spec_succ [in spec_succ]
spec_gcd_gt [in spec_gcd_gt]
spec_compare0_mn [in spec_compare0_mn]
spec_ww_mul [in spec_ww_mul]
spec_w_mul_add [in spec_w_mul_add]
spec_opp_carry [in spec_opp_carry]
spec_opp_carry [in spec_opp_carry]
spec_ww_karatsuba_c [in spec_ww_karatsuba_c]
spec_ww_mod [in spec_ww_mod]
spec_add_carry_c [in spec_add_carry_c]
spec_add_carry_c [in spec_add_carry_c]
spec_sqrt [in spec_sqrt]
spec_sqrt [in spec_sqrt]
spec_gcd_cont [in spec_gcd_cont]
spec_ww_is_zero [in spec_ww_is_zero]
spec_ww_gcd_gt_aux [in spec_ww_gcd_gt_aux]
spec_add_c [in spec_add_c]
spec_add_c [in spec_add_c]
spec_double_modn1 [in spec_double_modn1]
spec_ww_head00 [in spec_ww_head00]
spec_w_2 [in spec_w_2]
spec_opp [in spec_opp]
spec_opp [in spec_opp]
spec_sub_c [in spec_sub_c]
spec_sub_c [in spec_sub_c]
spec_double_0 [in spec_double_0]
spec_ww_mod_gt_eq [in spec_ww_mod_gt_eq]
spec_split [in spec_split]
spec_split [in spec_split]
spec_double_divn1_0 [in spec_double_divn1_0]
spec_add_carry [in spec_add_carry]
spec_add_carry [in spec_add_carry]
spec_gcd [in spec_gcd]
spec_gcd [in spec_gcd]
spec_ww_div_gt_aux [in spec_ww_div_gt_aux]
spec_to_Z_2 [in spec_to_Z_2]
spec_sub_carry_c [in spec_sub_carry_c]
spec_sub_carry_c [in spec_sub_carry_c]
spec_ww_tail0 [in spec_ww_tail0]
spec_ww_pred_c [in spec_ww_pred_c]
spec_ww_add_c_cont [in spec_ww_add_c_cont]
spec_ww_div21 [in spec_ww_div21]
spec_ww_opp_carry [in spec_ww_opp_carry]
spec_ww_add_carry_c [in spec_ww_add_carry_c]
spec_to_Z_pos [in spec_to_Z_pos]
spec_mul_add [in spec_mul_add]
spec_ww_succ [in spec_ww_succ]
spec_ww_mod_gt [in spec_ww_mod_gt]
spec_0 [in spec_0]
spec_0 [in spec_0]
spec_mul_c [in spec_mul_c]
spec_mul_c [in spec_mul_c]
spec_w_div32 [in spec_w_div32]
spec_mod [in spec_mod]
spec_ww_to_Z [in spec_ww_to_Z]
spec_ww_to_Z [in spec_ww_to_Z]
spec_div_gt [in spec_div_gt]
spec_more_than_1_digit [in spec_more_than_1_digit]
spec_more_than_1_digit [in spec_more_than_1_digit]
spec_extend_aux [in spec_extend_aux]
spec_ww_succ_c [in spec_ww_succ_c]
split_length_l [in split_length_l]
split_nth [in split_nth]
split_length_r [in split_length_r]
split_combine [in split_combine]
sqrt_main_trick [in sqrt_main_trick]
sqrt_more [in sqrt_more]
sqrt_sqrt [in sqrt_sqrt]
sqrt_le_0 [in sqrt_le_0]
sqrt_div_alt [in sqrt_div_alt]
sqrt_lem_1 [in sqrt_lem_1]
sqrt_positivity [in sqrt_positivity]
sqrt_continuity_pt_R1 [in sqrt_continuity_pt_R1]
sqrt_1 [in sqrt_1]
sqrt_iter_spec [in sqrt_iter_spec]
sqrt_0 [in sqrt_0]
sqrt_Rsqr [in sqrt_Rsqr]
sqrt_continuity_pt [in sqrt_continuity_pt]
sqrt_def [in sqrt_def]
sqrt_mult [in sqrt_mult]
sqrt_spec [in sqrt_spec]
sqrt_cauchy [in sqrt_cauchy]
sqrt_lt_0 [in sqrt_lt_0]
sqrt_lt_1 [in sqrt_lt_1]
sqrt_less_alt [in sqrt_less_alt]
sqrt_le_1_alt [in sqrt_le_1_alt]
sqrt_mult_alt [in sqrt_mult_alt]
sqrt_test_false [in sqrt_test_false]
sqrt_test_true [in sqrt_test_true]
sqrt_less [in sqrt_less]
sqrt_var_maj [in sqrt_var_maj]
sqrt_le_1 [in sqrt_le_1]
sqrt_main [in sqrt_main]
sqrt_lt_R0 [in sqrt_lt_R0]
sqrt_div [in sqrt_div]
sqrt_lem_0 [in sqrt_lem_0]
sqrt_Rsqr_abs [in sqrt_Rsqr_abs]
sqrt_eq_0 [in sqrt_eq_0]
sqrt_init [in sqrt_init]
sqrt_lt_1_alt [in sqrt_lt_1_alt]
sqrt_inj [in sqrt_inj]
sqrt_square [in sqrt_square]
sqrt_lt_0_alt [in sqrt_lt_0_alt]
sqrt_pos [in sqrt_pos]
sqrt2_neq_0 [in sqrt2_neq_0]
sqrt3_2_neq_0 [in sqrt3_2_neq_0]
sqrt31_step_correct [in sqrt31_step_correct]
sqrt31_step_def [in sqrt31_step_def]
sqrt312_step_correct [in sqrt312_step_correct]
sqrt312_step_def [in sqrt312_step_def]
sqrt312_lower_bound [in sqrt312_lower_bound]
sqr_pos [in sqr_pos]
square_spec [in square_spec]
square_not_prime [in square_not_prime]
Sstar_contains_Rstar [in Sstar_contains_Rstar]
star_monotone [in star_monotone]
StepFun_P45 [in StepFun_P45]
StepFun_P6 [in StepFun_P6]
StepFun_P44 [in StepFun_P44]
StepFun_P24 [in StepFun_P24]
StepFun_P9 [in StepFun_P9]
StepFun_P23 [in StepFun_P23]
StepFun_P1 [in StepFun_P1]
StepFun_P34 [in StepFun_P34]
StepFun_P13 [in StepFun_P13]
StepFun_P16 [in StepFun_P16]
StepFun_P17 [in StepFun_P17]
StepFun_P20 [in StepFun_P20]
StepFun_P14 [in StepFun_P14]
StepFun_P19 [in StepFun_P19]
StepFun_P32 [in StepFun_P32]
StepFun_P5 [in StepFun_P5]
StepFun_P38 [in StepFun_P38]
StepFun_P31 [in StepFun_P31]
StepFun_P8 [in StepFun_P8]
StepFun_P22 [in StepFun_P22]
StepFun_P11 [in StepFun_P11]
StepFun_P35 [in StepFun_P35]
StepFun_P28 [in StepFun_P28]
StepFun_P18 [in StepFun_P18]
StepFun_P3 [in StepFun_P3]
StepFun_P10 [in StepFun_P10]
StepFun_P33 [in StepFun_P33]
StepFun_P43 [in StepFun_P43]
StepFun_P12 [in StepFun_P12]
StepFun_P29 [in StepFun_P29]
StepFun_P21 [in StepFun_P21]
StepFun_P30 [in StepFun_P30]
StepFun_P26 [in StepFun_P26]
StepFun_P15 [in StepFun_P15]
StepFun_P46 [in StepFun_P46]
StepFun_P42 [in StepFun_P42]
StepFun_P2 [in StepFun_P2]
StepFun_P40 [in StepFun_P40]
StepFun_P4 [in StepFun_P4]
StepFun_P7 [in StepFun_P7]
StepFun_P36 [in StepFun_P36]
StepFun_P25 [in StepFun_P25]
StepFun_P37 [in StepFun_P37]
StepFun_P27 [in StepFun_P27]
StepFun_P41 [in StepFun_P41]
StepFun_P39 [in StepFun_P39]
Streicher_K__eq_rect_eq [in Streicher_K__eq_rect_eq]
strictincreasing_strictdecreasing_opp [in strictincreasing_strictdecreasing_opp]
StrictOrder_inverse [in StrictOrder_inverse]
StrictOrder_PartialOrder [in StrictOrder_PartialOrder]
StrictOrder_PreOrder [in StrictOrder_PreOrder]
Strict_Rel_Transitive [in Strict_Rel_Transitive]
Strict_super_set_contains_new_element [in Strict_super_set_contains_new_element]
Strict_Rel_Transitive_with_Rel_left [in Strict_Rel_Transitive_with_Rel_left]
Strict_Included_inv [in Strict_Included_inv]
Strict_Rel_Transitive_with_Rel [in Strict_Rel_Transitive_with_Rel]
Strict_Rel_is_Strict_Included [in Strict_Rel_is_Strict_Included]
Strict_inclusion_is_transitive_with_inclusion_left [in Strict_inclusion_is_transitive_with_inclusion_left]
Strict_Included_strict [in Strict_Included_strict]
Strict_inclusion_is_transitive_with_inclusion [in Strict_inclusion_is_transitive_with_inclusion]
Strict_Included_intro [in Strict_Included_intro]
Strict_inclusion_is_transitive [in Strict_inclusion_is_transitive]
strip_commut [in strip_commut]
StronglySorted_rect [in StronglySorted_rect]
StronglySorted_Sorted [in StronglySorted_Sorted]
StronglySorted_rec [in StronglySorted_rec]
StronglySorted_inv [in StronglySorted_inv]
Strong_confluence_direct [in Strong_confluence_direct]
Strong_confluence [in Strong_confluence]
Str_nth_tl_plus [in Str_nth_tl_plus]
Str_nth_tl_zipWith [in Str_nth_tl_zipWith]
Str_nth_plus [in Str_nth_plus]
Str_nth_tl_map [in Str_nth_tl_map]
Str_nth_zipWith [in Str_nth_zipWith]
Str_nth_map [in Str_nth_map]
SubEqui_P5 [in SubEqui_P5]
SubEqui_P7 [in SubEqui_P7]
SubEqui_P2 [in SubEqui_P2]
SubEqui_P6 [in SubEqui_P6]
SubEqui_P3 [in SubEqui_P3]
SubEqui_P4 [in SubEqui_P4]
SubEqui_P9 [in SubEqui_P9]
SubEqui_P8 [in SubEqui_P8]
SubEqui_P1 [in SubEqui_P1]
subrelation_symmetric [in subrelation_symmetric]
subrelation_refl [in subrelation_refl]
subrelation_respectful [in subrelation_respectful]
subrelation_proper [in subrelation_proper]
subset_types_imp_guarded_rel_choice_iff_rel_choice [in subset_types_imp_guarded_rel_choice_iff_rel_choice]
subset_eq [in subset_eq]
substring_correct2 [in substring_correct2]
substring_correct1 [in substring_correct1]
Subtract_intro [in Subtract_intro]
Subtract_inv [in Subtract_inv]
Sub_Add_new [in Sub_Add_new]
sub_carry [in sub_carry]
SuccNat2Pos.id_succ [in id_succ]
SuccNat2Pos.inj [in inj]
SuccNat2Pos.inj_iff [in inj_iff]
SuccNat2Pos.inj_compare [in inj_compare]
SuccNat2Pos.inj_succ [in inj_succ]
SuccNat2Pos.inv [in inv]
SuccNat2Pos.pred_id [in pred_id]
succ_plus_discr [in succ_plus_discr]
succ_IZR [in succ_IZR]
succ_pred [in succ_pred]
sum_growing [in sum_growing]
sum_N_predN [in sum_N_predN]
sum_inequa_Rle_lt [in sum_inequa_Rle_lt]
sum_maj1 [in sum_maj1]
sum_Rle [in sum_Rle]
sum_Ratan_seq_opp [in sum_Ratan_seq_opp]
sum_decomposition [in sum_decomposition]
sum_f_R0_triangle [in sum_f_R0_triangle]
sum_cv_maj [in sum_cv_maj]
sum_plus [in sum_plus]
sum_mul_carry [in sum_mul_carry]
sum_mul_carry [in sum_mul_carry]
sum_eq [in sum_eq]
sum_eq_R0 [in sum_eq_R0]
sum_cte [in sum_cte]
sum_incr [in sum_incr]
surjective_pairing [in surjective_pairing]
swap_Acc [in swap_Acc]
symmetric_equiv_inverse [in symmetric_equiv_inverse]
sym_EqSt [in sym_EqSt]
S_pred [in S_pred]
S_O_plus_INR [in S_O_plus_INR]
S_INR [in S_INR]