/top,rational_props_aux,exponentiation_aux,nn_root,root,nn_rational_expt,nnreal_expt,real_expt,nn_log,log,real_fun_power,ln_exp_def
structures/sort_array,permutations,min_array_def,min_seq,sort_seq,max_array_def,below_arrays,seqs,concat_arrays,sort_seq_lems,max_seq,permutations_seq,sort_array_def
reals/real_fun_preds,sigma_below_sub,abs_lems,sign,root,real_fun_ops,sigma_below,intervals_real,real_fun_props,sigma_upto,real_facts,sigma,sq
lnexp_fnd/ln_exp
analysis/step_fun_def,continuous_functions_props,lim_of_functions,derivatives,deriv_domain,top_sequences,deriv_domains,integral,step_fun_props,continuous_functions,continuity_interval,indefinite_integral,integral_split_scaf,inverse_continuous_functions,derivative_props,integral_cont_scaf,interval_minmax,integral_cont,step_fun_scaf,unif_cont_fun,fundamental_theorem,monotone_subsequence,convergence_ops,derivative_inverse,convergence_functions,deriv_domain_def,epsilon_lemmas,composition_continuous,integral_split,derivatives_def,partitions_scaf,continuous_functions_more,integral_step,real_fun_supinf,sequence_props,chain_rule,integral_bounded,integral_pulse,integral_def,integral_prep,lim_of_composition,convergence_sequences,continuity_props,derivatives_alt
finite_sets/func_composition,finite_sets_minmax,finite_sets_inductions,finite_sets_card_eq,finite_sets_below
ints/max_below
top:rational_props_aux,exponentiation_aux,nn_root,root,nn_rational_expt,nnreal_expt,real_expt,nn_log,log,real_fun_power,ln_exp_def
rational_props_aux:
exponentiation_aux:
nn_root:exponentiation_aux
root:reals@sign,nn_root
nn_rational_expt:rational_props_aux,nn_root
nnreal_expt:rational_props_aux,nn_root,nn_rational_expt
real_expt:nnreal_expt,root
nn_log:rational_props_aux,nn_root,nn_rational_expt,nnreal_expt
log:nn_log,real_expt
real_fun_power:reals@sign,real_expt
ln_exp_def:log,real_expt,lnexp_fnd@ln_exp,analysis@continuous_functions,analysis@derivatives