Sledgehammering... 
"mesh": Including 1000 relevant facts: power2_sum distrib_left_numeral power2_eq_square four_x_squared distrib_right_numeral one_power2 power_add mult.commute mult_2 semiring_normalization_rules(36) semiring_normalization_rules(29) semiring_normalization_rules(8) real_sqrt_pow2 mult_2_right semiring_norm(85) not_le semiring_norm(83) semigroup.intro add.right_neutral semiring_norm(11) left_add_twice semiring_norm(13) mult.assoc semiring_normalization_rules(4) mult.left_commute numeral_eq_iff add.left_neutral add.commute Let_numeral distrib_left semiring_norm(6) add_nonneg_nonneg mult_numeral_1 numeral_times_numeral real_sqrt_sum_squares_triangle_ineq semiring_norm(87) bounded_bilinear_def num.inject(1) numeral_plus_numeral semiring_norm(2) not_less mult_minus_right mult_numeral_left_semiring_numeral semiring_norm(12) L2_set_mult_ineq_lemma add_numeral_left linear ln_div comm_semiring_class.distrib power_add_numeral2 power_mult_numeral power_add_numeral abel_semigroup.intro left_add_mult_distrib mult_zero_left abel_semigroup_axioms.intro power_mult less_irrefl mult_cancel_left power_even_eq numeral_code(1) semiring_normalization_rules(26) dvd_refl real_sqrt_sum_squares_mult_squared_eq abel_semigroup.left_commute add_One_commute zero_le_power_eq_numeral power2_le_imp_le mult_nonneg_nonneg abs_of_nonneg ext sqrt_sum_squares_le_sum semiring_normalization_rules(31) add_mono_thms_linordered_semiring(1) le_add_same_cancel1 exp_bound add_diff_cancel_left' zero_less_numeral real_sqrt_sum_squares_ge1 mult.left_neutral semiring_normalization_rules(7) abel_semigroup.commute semiring_normalization_rules(13) zero_neq_numeral semiring_normalization_rules(20) zero_le_numeral One_nat_def semiring_normalization_rules(14) semiring_normalization_rules(21) semiring_normalization_rules(15) semiring_normalization_rules(16) mult_numeral_1_right distrib_right semiring_normalization_rules(17) add_left_cancel combine_common_factor power_mult_distrib semiring_normalization_rules(18) semiring_normalization_rules(22) power2_diff semiring_normalization_rules(19) semiring_normalization_rules(23) times_divide_eq_left numeral_Bit0 add.left_commute semiring_normalization_rules(25) is_num_normalize(1) mem_Collect_eq times_divide_eq_right Collect_mem_eq real_sqrt_abs sum_squares_bound Collect_cong comm_monoid_mult_class.mult_1 real_sqrt_sum_squares_mult_ge_zero real_sqrt_sum_squares_ge2 add_le_cancel_left semiring_1_class.of_nat_simps(2) add_Suc_right real_sqrt_four power_commutes arctan_add semiring_normalization_rules(24) add_diff_eq arctan_double add_mono_thms_linordered_field(5) semiring_norm(82) add_diff_cancel_left crossproduct_noteq power_numeral real_sqrt_ge_0_iff crossproduct_eq of_nat_0 real_sqrt_le_iff left_diff_distrib_numeral semiring_normalization_rules(1) real_sqrt_sum_squares_eq_cancel2 dbl_simps(5) add_diff_cancel_right' real_sqrt_sum_squares_eq_cancel powr_mult semiring_normalization_rules(34) diff_add_cancel cancel_comm_monoid_add_class.diff_cancel mult_eq_0_iff dbl_def power_commuting_commutes mult_zero_right powr_add semiring_normalization_rules(30) add_diff_cancel mult_minus_left num.distinct(1) order.trans arith_simps(16) not_numeral_le_zero ordered_ring_class.le_add_iff1 arith_simps(52) add_uminus_conv_diff power_one arsinh_real_def add_right_cancel order_refl sincos_total_2pi_le of_nat_numeral arsinh_real_aux powr_half_sqrt real_le_rsqrt power_zero_numeral sqrt_le_D diff_zero sincos_total_2pi le_divide_eq_numeral1(1) sqrt_sum_squares_le_sum_abs real_norm_def real_sqrt_ge_abs1 real_sqrt_ge_abs2 arctan_half sin_integer_2pi linordered_field_class.sign_simps(17) real_sqrt_eq_zero_cancel_iff zero_le_mult_iff id_apply semiring_norm(71) add_cancel_left_left add_cancel_left_right diff_le_eq semiring_norm(68) right_diff_distrib' real_exp_bound_lemma real_sqrt_eq_iff of_nat_eq_0_iff of_nat_power diff_minus_eq_add power_eq_0_iff right_diff_distrib le_add_same_cancel2 exp_lower_taylor_quadratic add_le_cancel_right eq_diff_eq monoseq_arctan_series numeral_le_iff add_mono_thms_linordered_field(1) eq_add_iff2 diff_eq_eq someI_ex mult_left_mono power_Suc less_imp_le mult_cancel_right cos_one_2pi_int arith_geo_mean_sqrt add_diff_cancel_right sqrt_def semiring_norm(69) eq_add_iff1 left_diff_distrib cos_integer_2pi le_add_diff_inverse diff_ge_0_iff_ge le_add_diff_inverse2 nat_induct sqrt_sum_squares_half_less summable_arctan_series real_sqrt_sum_squares_less add_mono_thms_linordered_semiring(3) antisym_conv zeroseq_arctan_series right_diff_distrib_numeral sum_power2_ge_zero split_mult_pos_le sin_two_pi arctan_series linordered_field_class.sign_simps(43) diff_diff_add abs_ln_one_plus_x_minus_x_bound linordered_field_class.sign_simps(42) cos_double_less_one linordered_field_class.sign_simps(16) abs_exp_cancel linordered_field_class.sign_simps(15) power2_abs exp_bound_lemma real_sqrt_le_mono diff_diff_eq2 real_sqrt_unique inverse_eq_divide nonzero_mult_div_cancel_right le_diff_eq divide_divide_eq_right zero_le_one add_le_imp_le_diff zero_le_power2 power2_nat_le_eq_le power2_nat_le_imp_le diff_add zero_le add_le_add_imp_diff_le le_real_sqrt_sumsq ordered_cancel_comm_monoid_diff_class.le_add_diff add.inverse_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 of_nat_mult mult.right_neutral ordered_cancel_comm_monoid_diff_class.add_diff_assoc ordered_cancel_comm_monoid_diff_class.diff_add_assoc ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 real_le_lsqrt bounded_bilinear.pos_bounded ordered_cancel_comm_monoid_diff_class.diff_add_assoc2 less_eq_real_def sum_power2_eq_zero_iff add.assoc abs_ln_one_plus_x_minus_x_bound_nonpos ordered_cancel_comm_monoid_diff_class.diff_diff_right real_sqrt_mult ordered_cancel_comm_monoid_diff_class.add_diff_inverse divide_divide_eq_left sin_times_pi_eq_0 ordered_cancel_comm_monoid_diff_class.le_imp_diff_is_add real_sqrt_power arith_geo_mean diff_right_commute complex_norm diff_eq_diff_less_eq real_less_lsqrt diff_right_mono eq_divide_eq_numeral1(1) abs_ge_zero diff_left_mono of_nat_eq_iff bounded_bilinear.bounded diff_mono cos_arctan diff_eq_diff_eq pow.simps(1) of_real_eq_id nat_diff_add_eq2 cos_x_y_le_one nat_diff_add_eq1 divide_eq_eq_numeral1(1) nat_le_add_iff2 semiring_norm(76) power2_commute nat_le_add_iff1 comm_monoid_add_class.add_0 DERIV_arctan_series nat_eq_add_iff2 nat_eq_add_iff1 linordered_field_class.sign_simps(39) Nat.add_diff_assoc2 linordered_field_class.sign_simps(38) Ints_mult linordered_field_class.sign_simps(37) ab_semigroup_add_class.add_ac(1) linordered_field_class.sign_simps(28) sincos_total_pi linordered_field_class.sign_simps(20) real_sqrt_pow2_iff linordered_field_class.sign_simps(19) linordered_field_class.sign_simps(26) of_nat_add linordered_field_class.sign_simps(3) sin_arctan linordered_field_class.sign_simps(1) add_pos_nonneg real_less_rsqrt power2_eq_imp_eq cos_arccos_lemma1 left_diff_distrib' add_mono_thms_linordered_field(4) divide_inverse linordered_field_class.sign_simps(34) Ints_cases linordered_field_class.sign_simps(33) mult_Suc_right sincos_total_pi_half linordered_field_class.sign_simps(32) zero_eq_power2 linordered_field_class.sign_simps(31) add_Suc complex_inverse linordered_field_class.sign_simps(30) not_sum_power2_lt_zero linordered_field_class.sign_simps(29) less_add_iff1 linordered_field_class.sign_simps(12) mult_0_right div_by_1 linordered_field_class.sign_simps(11) DERIV_arctan linordered_field_class.sign_simps(10) DERIV_cong linordered_field_class.sign_simps(9) add_mono_thms_linordered_field(3) log_def linordered_field_class.sign_simps(8) diff_0_right arcosh_real_def linordered_field_class.sign_simps(7) tanh_ln_real real_sqrt_less_iff power_divide order_trans log_mult zero_diff sqrt_ge_absD mult_Suc powr_one_gt_zero_iff arsinh_def le_less real_average_minus_second sin_arccos_lemma1 diff_add_eq nonzero_mult_div_cancel_left arith_special(3) diff_add_eq_diff_diff_swap le_0_eq diff_self power2_eq_iff_nonneg sin_arccos_abs real_average_minus_first zero_less_one add_implies_diff le0 sin_paired add_mono_thms_linordered_semiring(2) summable_Leibniz(1) arsinh_real_has_field_derivative add_mono ln_one_plus_pos_lower_bound add_left_mono diff_Suc_Suc power2_less_eq_zero_iff add_right_mono Suc_le_mono abs_ln_one_plus_x_minus_x_bound_nonneg le_iff_add divide_self_if add_le_imp_le_left add_le_imp_le_right sqrt_add_le_add_sqrt ordered_ring_class.le_add_iff2 cosh_ln_real sum_power2_le_zero_iff nat.inject zero_less_diff DERIV_const DERIV_fun_pow le_num_One_iff pos2 abs_divide monoid_axioms.intro ln_mult Suc_leI square_diff_square_factored zero_le_power not_one_le_zero power.simps(1) zero_power2 ab_group_add_class.ab_diff_conv_add_uminus monoid.intro linorder_neqE_linordered_idom times_complex.sel(2) tan_def add_mult_distrib bounded_bilinear.intro linordered_field_class.sign_simps(25) linordered_field_class.sign_simps(24) DERIV_powr linordered_field_class.sign_simps(23) add_le_mono norm_ge_zero linordered_field_class.sign_simps(6) linear_plus_1_le_power linordered_field_class.sign_simps(5) DERIV_power linordered_field_class.sign_simps(4) diff_gt_0_iff_gt ab_semigroup_mult_class.mult_ac(1) add_divide_distrib power_mono times_complex.sel(1) eq_divide_eq linordered_field_class.sign_simps(27) log_of_power_eq linordered_field_class.sign_simps(2) zero_le_square add_mono_thms_linordered_semiring(4) vector_space_assms(3) le_less_trans add.left_cancel monoid.left_neutral add.right_cancel tan_arctan add_left_imp_eq DERIV_fun_powr add_right_imp_eq add_strict_mono ln_one_minus_pos_lower_bound neq0_conv ring_class.ring_distribs(2) ring_class.ring_distribs(1) zero_le_even_power' complex_eq_iff linordered_field_class.sign_simps(36) linordered_field_class.sign_simps(35) atMost_iff linordered_field_class.sign_simps(18) less_le_trans max.cobounded2 mult_diff_mult of_nat_le_numeral_power_cancel_iff numeral_power_le_of_nat_cancel_iff power_odd_eq power2_minus Nat.add_diff_assoc power_Suc_0 bounded_bilinear.nonneg_bounded diff_diff_left of_int_numeral real_of_nat_eq_numeral_power_cancel_iff odd_0_le_power_imp_0_le less_numeral_extra(3) Nat.diff_diff_right add_divide_eq_if_simps(1) nat_add_left_cancel_le minus_apply Maclaurin_sin_expansion2 sum_power2_gt_zero_iff numeral_2_eq_2 realpow_square_minus_le zero_less_abs_iff sinh_ln_real Let_0 one_le_mult_iff mult_0 le_zero_eq zero_less_Suc UNIV_I real_divide_square_eq linorder_cases square_diff_one_factored zero_eq_add_iff_both_eq_0 add_eq_0_iff_both_eq_0 Maclaurin_sin_expansion add_cancel_right_right real_mult_less_iff1 cmod_def add_cancel_right_left linorder_neqE_nat not_real_square_gt_zero cos_arccos_abs real_sqrt_abs2 real_mult_le_cancel_iff2 real_scaleR_def double_zero_sym double_zero vector_space_assms(2) ln_sqrt real_mult_le_cancel_iff1 ln_eq_zero_iff one_less_numeral_iff diff_diff_cancel zero_less_mult_iff abs_eq_0 of_nat_less_numeral_power_cancel_iff Maclaurin_sin_expansion4 real_sqrt_zero less_divide_eq_numeral1(1) numeral_power_less_of_nat_cancel_iff add.inverse_neutral zero_le_double_add_iff_zero_le_single_add not_less_zero Re_divide double_add_le_zero_iff_single_add_le_zero abs_power2 vector_space_assms(4) add_le_same_cancel2 numeral_power_eq_of_nat_cancel_iff Maclaurin_minus_cos_expansion add_le_same_cancel1 zero_less_power2 less_induct Maclaurin_sin_expansion3 nat_one_le_power sum_squares_eq_zero_iff less_trans Maclaurin_cos_expansion diff_add_zero add_2_eq_Suc add_2_eq_Suc' Maclaurin_cos_expansion2 real_sqrt_le_0_iff reals_Archimedean3 le_neq_trans of_nat_sum cmod_power2 monoid.right_neutral Nat.ex_has_greatest_nat zero_reorient nat_le_linear diff_le_mono2 realpow_pos_nth2 division_ring_divide_zero powr_diff le_diff_iff' diff_le_self diff_le_mono inverse_complex.sel(1) Nat.diff_diff_eq nat.simps(3) diff_commute Suc_numeral numeral.simps(3) le_diff_iff eq_diff_iff lessI le_antisym sin_arccos eq_imp_le cos_periodic le_trans sin_periodic le_refl inverse_complex.sel(2) pos_add_strict semigroup.assoc le_numeral_extra(3) semiring_normalization_rules(9) tan_periodic semiring_normalization_rules(10) uminus_add_conv_diff mult_right_cancel mult_divide_mult_cancel_left_if add_divide_eq_if_simps(4) mult_left_cancel sums_if no_zero_divisors mult_less_cancel_left_pos cos_arcsin divisors_zero one_less_log_cancel_iff mult_not_zero mult_pos_pos Im_divide add_0_iff log_less_one_cancel_iff semiring_normalization_rules(5) add_le_less_mono divide_minus_left semiring_normalization_rules(6) add.group_left_neutral add.comm_neutral less_imp_neq binomial less_linear Im_power2 numeral_1_eq_Suc_0 eq_iff_diff_eq_0 cot_periodic power_not_zero abs_mult ordered_comm_semiring_class.comm_mult_left_mono cos_add of_nat_less_two_power linordered_comm_semiring_strict_class.comm_mult_strict_left_mono powr_numeral mult_nonneg_nonpos2 less_le DERIV_const_average mult_nonpos_nonneg dual_order.order_iff_strict mult_nonneg_nonpos real_minus_mult_self_le split_mult_neg_le not_less_iff_gr_or_eq mult_le_0_iff not_numeral_less_zero less_add_iff2 cis_mult mult_right_mono mult_right_mono_neg divide_eq_0_iff complex_eq_0 mult_nonpos_nonpos mult_left_mono_neg lemma_termdiff3 mult_1s(3) tanh_def mult_mono' mult_mono odd_power_less_zero power2_less_imp_less one_le_power add_nonpos_eq_0_iff binomial_r_part_sum add_nonneg_eq_0_iff of_int_minus add_nonpos_nonpos Parity.ring_1_class.power_minus_even add_increasing2 complex_mult_cnj add_decreasing2 power_minus_odd add_increasing DERIV_arcsin add_decreasing arcosh_def power2_less_0 complex_neq_0 numeral_times_minus_swap le_iff_diff_le_0 add_scale_eq_noteq rcis_def BitM.simps(1) abs_le_square_iff real_sqrt_eq_zero_cancel Complex_divide real_sqrt_ge_zero num.rec(1) le_funD minus_mult_commute le_funE of_real_mult le_funI DERIV_arccos le_fun_def minus_mult_right order_subst1 add_self_div_2 order_subst2 ord_eq_le_subst ord_le_eq_subst eq_iff complex_unit_circle antisym complex_surj artanh_real_has_field_derivative eq_refl sqrt2_less_2 arcosh_real_has_field_derivative le_cases real_archimedian_rdiv_eq_0 neg_0_less_iff_less lemma_real_divide_sqrt_less inverse_numeral_1 le_cases3 rcis_mult arith_simps(19) ord_eq_le_trans nat_numeral ord_le_eq_trans cos_ge_zero order_class.order.antisym realpow_pos_nth divide_le_eq not_gr0 exp_first_two_terms dual_order.refl linorder_wlog arith_simps(55) dual_order.trans realpow_pos_nth_unique dual_order.antisym real_root_pos_unique sum_squares_le_zero_iff sin_add sum_squares_ge_zero sin_2npi fun_diff_def cos_2npi complete_real div2_Suc_Suc mult_strict_mono' cos_double nat_add_right_cancel arcsin nat_add_left_cancel of_int_eq_iff Nat.le_imp_diff_is_add diff_add_inverse2 nat_0_less_mult_iff mult_le_cancel_left_pos add_frac_eq diff_add_inverse power_eq_imp_eq_base divide_complex_def Nat.diff_add_assoc2 add_gr_0 cos_one_2pi nat_le_iff_add diff_0 Nat.diff_add_assoc cos_pi trans_le_add2 sin_pi trans_le_add1 cos_tan Nat.le_diff_conv2 inverse_complex.ctr le_diff_conv ex_power_ivl2 diff_cancel2 add_le_mono1 sin_tan Nat.le_add_diff exp_ln Nat.diff_cancel Suc_pred le_Suc_ex zero_neq_one add_leD2 semiring_norm(75) of_real_eq_0_iff add_leD1 cis.sel(2) le_add2 cis.sel(1) le_add1 sin_int_2pin add_leE floor_log_nat_eq_if le_cube cos_pi_half le_square semiring_norm(78) sin_pi_half mult_le_mono cos_int_2pin mult_le_mono1 less_2_cases mult_le_mono2 ex_power_ivl1 diff_mult_distrib vector_space_assms(1) diff_mult_distrib2 rel_fun_eq floor_log_nat_eq_powr_iff of_nat_id cos_paired cos_arccos zero_complex.sel(1) zero_complex.sel(2) sin_ge_zero Suc_n_div_2_gt_zero is_equality_def add_diff_add is_equality_eq sum.cong atLeastAtMost_iff transfer_start sin_arcsin div_2_gt_zero Rel_def add_mult_distrib2 ceiling_log_nat_eq_if exp_two_pi_i exp_two_pi_i' sin_cos_squared_add2 arccos_cos_eq_abs_2pi bij_betw_roots_unity lemma_MVT ceiling_log_nat_eq_powr_iff arccos_bounded Let_Suc divide_pos_pos pi_series pi_neq_zero old.nat.inject Rel_abs arctan_one add_is_0 Nat.add_0_right eventually_True abs_abs even_diff_nat abs_idempotent Rel_app diff_0_eq_0 cos_minus diff_self_eq_0 of_real_power nat_mult_div_cancel_disj mult_cancel2 powr_neg_numeral mult_cancel1 choose_square_sum Real_Vector_Spaces.linear_def mult_is_0 sin_minus not_gr_zero sum_split_even_odd add_less_cancel_left add_less_cancel_right numeral_less_iff div_0 abs_le_iff div_by_0 complex_eqI vector_space.intro of_nat_0_eq_iff powr_realpow sin_double of_nat_less_iff square_le_1 abs_0 has_derivative_arctan abs_0_eq inverse_eq_divide_numeral abs_zero cos_npi abs_mult_self_eq cos_limit_1 power_Suc0_right eq_diff_eq' abs_add_abs vector_space.vector_space_assms(2) abs_numeral real_add_less_0_iff real_0_less_add_iff abs_of_nat sin_bound_lemma Suc_diff_diff mult_eq_1_iff sin_squared_eq one_eq_mult_iff of_nat_eq_id diff_is_0_eq vector_space.vector_space_assms(3) diff_is_0_eq' Suc_eq_plus1 odd_real_root_unique nat_power_eq_Suc_0_iff at_right_to_0 sin_expansion_lemma add_less_same_cancel1 real_add_le_0_iff add_less_same_cancel2 real_0_le_add_iff less_add_same_cancel1 gbinomial_r_part_sum less_add_same_cancel2 power2_i double_add_less_zero_iff_single_add_less_zero imageE zero_less_double_add_iff_zero_less_single_add has_real_derivative_pos_inc_right add_divide_eq_iff tan_periodic_n of_nat_le_0_iff of_nat_0_less_iff odd_real_root_power_cancel abs_le_zero_iff transfer_implies_transfer(1) abs_le_self_iff module.intro cos_squared_eq Real.positive_add power_0_Suc central_binomial_lower_bound of_nat_le_iff cos_diff_limit_1 plus_inverse_ge_2 cos_expansion_lemma complex_add DERIV_pos_inc_right of_real_add summable_Leibniz(5) num_eq_iff real_sqrt_gt_0_iff cnj_add_mult_eq_Re real_sqrt_lt_0_iff DERIV_compose_FDERIV neg_less_iff_less of_nat_eq_of_nat_power_cancel_iff subsetI of_nat_power_eq_of_nat_cancel_iff vector_space.vector_space_assms(4) real_sqrt_mult_self dvdE divide_le_eq_numeral1(1) equalityI vector_space.vector_space_assms(1) DERIV_neg_dec_right divide_less_eq_numeral1(1) minus_add of_nat_zero_less_power_iff module_hom_eq_linear zero_less_power_abs_iff empty_iff pred_numeral_simps(2) numeral_le_real_of_nat_iff oddE diff_Suc_diff_eq1 diff_Suc_diff_eq2 cosh_def of_nat_power_less_of_nat_cancel_iff cosh_double of_nat_less_of_nat_power_cancel_iff sin_npi evenE real.right_total num.rec(2) fact_double even_add of_nat_le_of_nat_power_cancel_iff of_nat_power_le_of_nat_cancel_iff Domainp_pcr_real arccos_1 neg_0_le_iff_le cos_le_one zmod_numeral_Bit1 summable_Leibniz'(5) add_is_1 pos_zdiv_mult_2 one_is_add max.bounded_iff abs_not_less_zero complex_of_real_add_Complex abs_of_pos sin_periodic_pi2 real_of_nat_div4 Complex_add_complex_of_real real_of_nat_div2 two_realpow_ge_one nat.distinct(1) old.nat.distinct(2) complex_mod_mult_cnj old.nat.distinct(1) cos_ge_minus_one nat.discI pochhammer_double Suc_inject machin_Euler cos_zero diff_induct plus_real.transfer n_not_Suc_n nat_of_num_add
"mepo": Including 1000 relevant facts: distrib_left_numeral distrib_right_numeral power2_sum four_x_squared semiring_normalization_rules(36) semiring_normalization_rules(29) power2_eq_square semiring_norm(85) semiring_norm(83) mult_2 mult_2_right left_add_twice numeral_eq_iff Let_numeral semiring_norm(6) semiring_norm(13) semiring_norm(87) num.inject(1) semiring_norm(11) semiring_norm(12) numeral_times_numeral mult_numeral_left_semiring_numeral numeral_plus_numeral add_numeral_left semiring_norm(2) power_mult_numeral power_add_numeral2 power_add_numeral left_add_mult_distrib add_One_commute power_mult semiring_normalization_rules(31) power_add semiring_normalization_rules(26) power_even_eq semiring_normalization_rules(7) semiring_normalization_rules(13) semiring_normalization_rules(14) semiring_normalization_rules(15) semiring_normalization_rules(16) semiring_normalization_rules(17) semiring_normalization_rules(18) semiring_normalization_rules(19) semiring_normalization_rules(20) semiring_normalization_rules(21) mem_Collect_eq Collect_mem_eq Collect_cong ext semiring_normalization_rules(22) semiring_normalization_rules(23) semiring_normalization_rules(24) semiring_normalization_rules(25) is_num_normalize(1) semiring_norm(82) crossproduct_noteq crossproduct_eq semiring_normalization_rules(1) semiring_normalization_rules(8) semiring_normalization_rules(34) power_commuting_commutes power_mult_distrib power_commutes semiring_normalization_rules(30) num.distinct(1) mult_numeral_1_right mult_numeral_1 numeral_Bit0 power_numeral add_right_cancel add_left_cancel L2_set_mult_ineq_lemma sum_squares_bound power2_diff real_sqrt_sum_squares_mult_squared_eq combine_common_factor distrib_right distrib_left comm_semiring_class.distrib linordered_field_class.sign_simps(17) semiring_norm(71) semiring_norm(68) real_sqrt_eq_iff add_le_cancel_left add_le_cancel_right numeral_le_iff add_diff_cancel diff_add_cancel add_diff_cancel_left add_diff_cancel_left' add_diff_cancel_right add_diff_cancel_right' semiring_norm(69) real_sqrt_le_iff le_add_diff_inverse le_add_diff_inverse2 left_diff_distrib_numeral right_diff_distrib_numeral real_sqrt_four linordered_field_class.sign_simps(43) linordered_field_class.sign_simps(42) linordered_field_class.sign_simps(16) linordered_field_class.sign_simps(15) real_sqrt_le_mono diff_le_eq le_diff_eq add_le_imp_le_diff diff_add add_le_add_imp_diff_le ordered_cancel_comm_monoid_diff_class.le_add_diff ordered_cancel_comm_monoid_diff_class.le_diff_conv2 ordered_cancel_comm_monoid_diff_class.add_diff_assoc ordered_cancel_comm_monoid_diff_class.diff_add_assoc ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 ordered_cancel_comm_monoid_diff_class.diff_add_assoc2 ordered_cancel_comm_monoid_diff_class.diff_diff_right ordered_cancel_comm_monoid_diff_class.add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_imp_diff_is_add diff_right_commute diff_eq_diff_less_eq diff_right_mono diff_left_mono diff_mono diff_eq_diff_eq nat_diff_add_eq2 nat_diff_add_eq1 nat_le_add_iff2 nat_le_add_iff1 nat_eq_add_iff2 nat_eq_add_iff1 linordered_field_class.sign_simps(39) linordered_field_class.sign_simps(38) linordered_field_class.sign_simps(37) linordered_field_class.sign_simps(20) linordered_field_class.sign_simps(19) left_diff_distrib right_diff_distrib left_diff_distrib' right_diff_distrib' linordered_field_class.sign_simps(34) linordered_field_class.sign_simps(33) linordered_field_class.sign_simps(32) linordered_field_class.sign_simps(31) linordered_field_class.sign_simps(30) linordered_field_class.sign_simps(29) linordered_field_class.sign_simps(12) linordered_field_class.sign_simps(11) linordered_field_class.sign_simps(10) linordered_field_class.sign_simps(9) linordered_field_class.sign_simps(8) linordered_field_class.sign_simps(7) diff_eq_eq eq_diff_eq add_diff_eq diff_diff_eq2 diff_add_eq diff_add_eq_diff_diff_swap diff_diff_add add_implies_diff add_mono_thms_linordered_semiring(3) add_mono_thms_linordered_semiring(2) add_mono_thms_linordered_semiring(1) add_mono add_left_mono add_right_mono le_iff_add add_le_imp_le_left add_le_imp_le_right ordered_ring_class.le_add_iff1 ordered_ring_class.le_add_iff2 le_real_sqrt_sumsq real_sqrt_mult real_sqrt_power le_num_One_iff eq_add_iff1 eq_add_iff2 square_diff_square_factored sqrt_le_D real_le_rsqrt real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2 real_sqrt_sum_squares_triangle_ineq pow.simps(1) power2_nat_le_eq_le power2_nat_le_imp_le linordered_field_class.sign_simps(25) linordered_field_class.sign_simps(24) linordered_field_class.sign_simps(23) linordered_field_class.sign_simps(6) linordered_field_class.sign_simps(5) linordered_field_class.sign_simps(4) ab_semigroup_mult_class.mult_ac(1) mult.assoc mult.commute mult.left_commute ab_semigroup_add_class.add_ac(1) linordered_field_class.sign_simps(28) linordered_field_class.sign_simps(27) linordered_field_class.sign_simps(26) linordered_field_class.sign_simps(3) linordered_field_class.sign_simps(2) linordered_field_class.sign_simps(1) add_mono_thms_linordered_semiring(4) add.assoc add.left_cancel add.right_cancel add.commute add.left_commute add_left_imp_eq add_right_imp_eq power2_commute ring_class.ring_distribs(2) ring_class.ring_distribs(1) linordered_field_class.sign_simps(36) linordered_field_class.sign_simps(35) linordered_field_class.sign_simps(18) mult_diff_mult real_sqrt_sum_squares_mult_ge_zero Nat.add_diff_assoc diff_diff_left Nat.add_diff_assoc2 Nat.diff_diff_right nat_add_left_cancel_le minus_apply order_refl real_sqrt_pow2 Let_0 le_zero_eq mult_cancel_right mult_cancel_left mult_eq_0_iff mult_zero_right mult_zero_left zero_eq_add_iff_both_eq_0 add_eq_0_iff_both_eq_0 add_cancel_right_right add_cancel_right_left add_cancel_left_right add_cancel_left_left double_zero_sym double_zero add.right_neutral add.left_neutral diff_self diff_0_right zero_diff diff_zero cancel_comm_monoid_add_class.diff_cancel diff_diff_cancel real_sqrt_eq_zero_cancel_iff real_sqrt_zero zero_le_double_add_iff_zero_le_single_add double_add_le_zero_iff_single_add_le_zero le_add_same_cancel2 le_add_same_cancel1 add_le_same_cancel2 add_le_same_cancel1 diff_ge_0_iff_ge sum_squares_eq_zero_iff diff_add_zero power_zero_numeral real_sqrt_le_0_iff real_sqrt_ge_0_iff zero_eq_power2 power2_eq_iff_nonneg power2_less_eq_zero_iff sum_power2_eq_zero_iff real_sqrt_pow2_iff Nat.ex_has_greatest_nat zero_reorient nat_le_linear diff_le_mono2 le_diff_iff' diff_le_self diff_le_mono Nat.diff_diff_eq diff_commute le_diff_iff eq_diff_iff le_antisym eq_imp_le le_trans le_refl zero_le le_numeral_extra(3) semiring_normalization_rules(9) semiring_normalization_rules(10) mult_right_cancel mult_left_cancel no_zero_divisors divisors_zero mult_not_zero add_0_iff semiring_normalization_rules(5) semiring_normalization_rules(6) add.group_left_neutral add.comm_neutral comm_monoid_add_class.add_0 zero_neq_numeral eq_iff_diff_eq_0 power_not_zero ordered_comm_semiring_class.comm_mult_left_mono zero_le_mult_iff mult_nonneg_nonpos2 mult_nonpos_nonneg mult_nonneg_nonpos mult_nonneg_nonneg split_mult_neg_le mult_le_0_iff mult_right_mono mult_right_mono_neg mult_left_mono mult_nonpos_nonpos mult_left_mono_neg split_mult_pos_le zero_le_square mult_mono' mult_mono add_nonpos_eq_0_iff add_nonneg_eq_0_iff add_nonpos_nonpos add_nonneg_nonneg add_increasing2 add_decreasing2 add_increasing add_decreasing zero_le_numeral not_numeral_le_zero le_iff_diff_le_0 add_scale_eq_noteq power_mono zero_le_power real_sqrt_eq_zero_cancel real_sqrt_ge_zero le_funD le_funE le_funI le_fun_def order_subst1 order_subst2 ord_eq_le_subst ord_le_eq_subst eq_iff antisym linear eq_refl le_cases order.trans le_cases3 antisym_conv ord_eq_le_trans ord_le_eq_trans order_class.order.antisym order_trans dual_order.refl linorder_wlog dual_order.trans dual_order.antisym sum_squares_le_zero_iff sum_squares_ge_zero fun_diff_def complete_real nat_add_right_cancel nat_add_left_cancel Nat.le_imp_diff_is_add diff_add_inverse2 diff_add_inverse Nat.diff_add_assoc2 nat_le_iff_add Nat.diff_add_assoc trans_le_add2 trans_le_add1 Nat.le_diff_conv2 le_diff_conv diff_cancel2 add_le_mono1 Nat.le_add_diff Nat.diff_cancel add_le_mono le_Suc_ex add_leD2 add_leD1 le_add2 le_add1 add_leE le_cube le_square mult_le_mono mult_le_mono1 mult_le_mono2 diff_mult_distrib diff_mult_distrib2 sqrt_add_le_add_sqrt zero_power2 power2_le_imp_le power2_eq_imp_eq zero_le_power2 sum_power2_le_zero_iff sum_power2_ge_zero zero_le_even_power' add_diff_add real_sqrt_unique real_le_lsqrt real_sqrt_sum_squares_eq_cancel2 real_sqrt_sum_squares_eq_cancel add_mult_distrib add_mult_distrib2 sqrt_sum_squares_le_sum arith_geo_mean arith_geo_mean_sqrt real_less_lsqrt of_nat_le_numeral_power_cancel_iff numeral_power_le_of_nat_cancel_iff odd_0_le_power_imp_0_le sqrt_sum_squares_le_sum_abs Let_Suc nat.inject old.nat.inject of_nat_eq_iff le0 add_is_0 Nat.add_0_right abs_abs abs_idempotent diff_0_eq_0 diff_self_eq_0 nat_mult_div_cancel_disj mult_cancel2 mult_cancel1 mult_0_right mult_is_0 not_gr_zero add_less_cancel_left add_less_cancel_right numeral_less_iff div_0 div_by_0 of_nat_eq_0_iff of_nat_0_eq_iff of_nat_0 of_nat_less_iff abs_0 abs_0_eq abs_eq_0 abs_zero abs_mult_self_eq power_Suc0_right abs_add_abs abs_numeral Suc_le_mono add_Suc_right abs_of_nat diff_Suc_Suc Suc_diff_diff mult_eq_1_iff one_eq_mult_iff diff_is_0_eq diff_is_0_eq' real_divide_square_eq real_sqrt_less_iff nat_power_eq_Suc_0_iff power_Suc_0 add_less_same_cancel1 add_less_same_cancel2 less_add_same_cancel1 less_add_same_cancel2 double_add_less_zero_iff_single_add_less_zero zero_less_double_add_iff_zero_less_single_add diff_gt_0_iff_gt nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right of_nat_le_0_iff of_nat_0_less_iff abs_le_zero_iff abs_le_self_iff abs_of_nonneg zero_less_abs_iff power_0_Suc of_nat_le_iff of_nat_numeral of_nat_add of_nat_mult not_real_square_gt_zero real_mult_less_iff1 one_le_mult_iff mult_Suc_right real_sqrt_gt_0_iff real_sqrt_lt_0_iff of_nat_power of_nat_eq_of_nat_power_cancel_iff of_nat_power_eq_of_nat_cancel_iff real_sqrt_mult_self real_sqrt_abs2 divide_le_eq_numeral1(1) le_divide_eq_numeral1(1) divide_eq_eq_numeral1(1) eq_divide_eq_numeral1(1) divide_less_eq_numeral1(1) less_divide_eq_numeral1(1) of_nat_zero_less_power_iff zero_less_power_abs_iff real_mult_le_cancel_iff1 real_mult_le_cancel_iff2 numeral_le_real_of_nat_iff diff_Suc_diff_eq1 diff_Suc_diff_eq2 of_nat_power_less_of_nat_cancel_iff of_nat_less_of_nat_power_cancel_iff Suc_numeral abs_power2 power2_abs add_2_eq_Suc add_2_eq_Suc' of_nat_le_of_nat_power_cancel_iff of_nat_power_le_of_nat_cancel_iff numeral_power_eq_of_nat_cancel_iff real_of_nat_eq_numeral_power_cancel_iff zero_less_power2 numeral_power_less_of_nat_cancel_iff of_nat_less_numeral_power_cancel_iff real_sqrt_abs add_is_1 one_is_add abs_not_less_zero abs_of_pos real_of_nat_div4 real_of_nat_div2 nat.distinct(1) old.nat.distinct(2) old.nat.distinct(1) nat.discI Suc_inject nat_induct diff_induct n_not_Suc_n zero_induct Suc_neq_Zero Zero_neq_Suc Zero_not_Suc measure_induct old.nat.exhaust not0_implies_Suc measure_induct_rule ord_eq_less_subst ord_less_eq_subst order_less_subst1 order_less_subst2 lt_ex gt_ex neqE neq_iff order.asym dense lift_Suc_mono_less less_imp_neq less_asym less_asym' less_trans less_linear less_irrefl ord_eq_less_trans ord_less_eq_trans dual_order.asym less_imp_not_eq less_not_sym less_induct lift_Suc_mono_less_iff of_nat_neq_0 antisym_conv3 less_imp_not_eq2 less_imp_triv linorder_cases dual_order.irrefl order.strict_trans less_imp_not_less exists_least_iff linorder_less_wlog dual_order.strict_trans not_less_iff_gr_or_eq order.strict_implies_not_eq dual_order.strict_implies_not_eq of_nat_less_0_iff less_imp_of_nat_less of_nat_less_imp_less linorder_neqE_linordered_idom abs_mult_less dense_eq0_I abs_diff_less_iff reals_Archimedean3 realpow_pos_nth2 numeral_1_eq_Suc_0 abs_ge_self abs_le_D1 abs_eq_0_iff abs_mult abs_minus_commute power_abs mult_of_nat_commute nat_one_le_power order.not_eq_order_implies_strict dual_order.strict_implies_order dual_order.strict_iff_order dual_order.order_iff_strict order.strict_implies_order dense_le_bounded dense_ge_bounded dual_order.strict_trans2 dual_order.strict_trans1 order.strict_iff_order order.order_iff_strict order.strict_trans2 order.strict_trans1 not_le_imp_less less_le_not_le le_imp_less_or_eq le_less_linear dense_le dense_ge less_le_trans le_less_trans antisym_conv2 antisym_conv1 less_imp_le le_neq_trans not_less not_le order_less_le_subst2 order_less_le_subst1 order_le_less_subst2 order_le_less_subst1 less_le le_less leI leD less_numeral_extra(3) field_lbound_gt_zero gr_zeroI not_less_zero gr_implies_not_zero zero_less_iff_neq_zero power_divide add_mono_thms_linordered_field(5) add_mono_thms_linordered_field(2) add_mono_thms_linordered_field(1) add_strict_mono add_strict_left_mono add_strict_right_mono add_less_imp_less_left add_less_imp_less_right diff_strict_right_mono diff_strict_left_mono diff_eq_diff_less diff_strict_mono Suc_leD le_SucE le_SucI Suc_le_D le_Suc_eq Suc_n_not_le_n not_less_eq_eq full_nat_induct nat_induct_at_least transitive_stepwise_le add_Suc_shift add_Suc zero_induct_lemma Suc_mult_cancel1 less_eq_real_def real_sqrt_divide real_sqrt_less_mono less_eq_nat.simps(1) le_0_eq plus_nat.add_0 add_eq_self_zero diffs0_imp_equal minus_nat.diff_0 nat_mult_eq_cancel_disj mult_0 divide_less_eq_numeral(1) less_divide_eq_numeral(1) power_strict_mono numeral_2_eq_2 le_divide_eq_numeral(1) divide_le_eq_numeral(1) of_nat_less_two_power abs_ge_zero half_gt_zero half_gt_zero_iff abs_triangle_ineq field_less_half_sum abs_triangle_ineq2_sym abs_triangle_ineq3 abs_triangle_ineq2 of_nat_0_le_iff of_nat_mono divide_numeral_1 linordered_field_class.sign_simps(45) linordered_field_class.sign_simps(44) mult_neg_neg not_square_less_zero mult_less_0_iff mult_neg_pos mult_pos_neg mult_pos_pos mult_pos_neg2 zero_less_mult_iff zero_less_mult_pos zero_less_mult_pos2 mult_less_cancel_left_neg mult_less_cancel_left_pos mult_strict_left_mono_neg mult_strict_left_mono mult_less_cancel_left_disj mult_strict_right_mono_neg mult_strict_right_mono mult_less_cancel_right_disj linordered_comm_semiring_strict_class.comm_mult_strict_left_mono add_mono_thms_linordered_field(4) add_mono_thms_linordered_field(3) add_le_less_mono add_less_le_mono add_less_zeroD add_neg_neg add_pos_pos pos_add_strict not_numeral_less_zero zero_less_numeral semiring_normalization_rules(28) semiring_normalization_rules(27) power_Suc power_Suc2 less_iff_diff_less_0 lift_Suc_antimono_le lift_Suc_mono_le zero_less_power linordered_field_class.sign_simps(41) linordered_field_class.sign_simps(40) linordered_field_class.sign_simps(14) linordered_field_class.sign_simps(13) diff_less_eq less_diff_eq linordered_semidom_class.add_diff_inverse Suc_diff_le Suc_mult_le_cancel1 mult_Suc real_sqrt_sum_squares_less real_sqrt_gt_zero diff_add_0 lemma_real_divide_sqrt_less abs_mult_pos abs_eq_mult zero_le_power_abs abs_diff_le_iff abs_triangle_ineq4 abs_diff_triangle_ineq odd_power_less_zero divide_eq_eq_numeral(1) eq_divide_eq_numeral(1) of_nat_diff power_inject_base power_le_imp_le_base mult_le_cancel_left mult_le_cancel_right mult_left_less_imp_less mult_strict_mono mult_less_cancel_left mult_right_less_imp_less mult_strict_mono' mult_less_cancel_right mult_le_cancel_left_neg mult_le_cancel_left_pos mult_left_le_imp_le mult_right_le_imp_le mult_le_less_imp_less mult_less_le_imp_less add_neg_nonpos add_nonneg_pos add_nonpos_neg add_pos_nonneg add_strict_increasing add_strict_increasing2 not_sum_squares_lt_zero sum_squares_gt_zero_iff power_less_imp_less_base less_add_iff1 less_add_iff2 real_div_sqrt field_sum_of_halves power_diff Suc_nat_number_of_add sqrt2_less_2 sqrt_sum_squares_half_less abs_le_square_iff power2_less_0 real_less_rsqrt sqrt_ge_absD power2_less_imp_less power_odd_eq not_sum_power2_lt_zero sum_power2_gt_zero_iff real_sqrt_ge_abs1 real_sqrt_ge_abs2 real_average_minus_first real_average_minus_second add_self_div_2 div2_Suc_Suc zero_le_divide_abs_iff division_ring_divide_zero divide_cancel_right divide_cancel_left divide_eq_0_iff times_divide_eq_left divide_divide_eq_left divide_divide_eq_right times_divide_eq_right neq0_conv Suc_less_eq Suc_mono lessI abs_divide nat_add_left_cancel_less semiring_norm(78) semiring_norm(75) mult_divide_mult_cancel_left_if nonzero_mult_divide_mult_cancel_left nonzero_mult_divide_mult_cancel_left2 nonzero_mult_divide_mult_cancel_right nonzero_mult_divide_mult_cancel_right2 div_mult_mult1 div_mult_mult2 div_mult_mult1_if zero_less_Suc less_Suc0 add_gr_0 zero_less_diff nat_mult_less_cancel_disj nat_0_less_mult_iff mult_less_cancel2 div_by_Suc_0 div_less nat_zero_less_power_iff semiring_norm(76) div_mult_self4 div_mult_self3 div_mult_self2 div_mult_self1 divide_le_0_abs_iff power_eq_0_iff Suc_pred mult_le_cancel2 nat_mult_le_cancel_disj div_mult_self_is_m div_mult_self1_is_m real_of_nat_less_numeral_iff numeral_less_real_of_nat_iff mult_less_mono1 mult_less_mono2 less_imp_add_positive nat_mult_div_cancel1 div_greater_zero_iff div_le_mono2 less_fun_def ex_least_nat_le diff_less gr0I lessE not_gr0 Suc_lessD Suc_lessE Suc_lessI less_SucE less_SucI not_less0 less_zeroE Ex_less_Suc less_Suc_eq nat_neq_iff not_less_eq All_less_Suc Ex_less_Suc2 Suc_less_eq2 gr0_conv_Suc less_antisym All_less_Suc2 Suc_less_SucD less_not_refl less_not_refl2 less_not_refl3 less_trans_Suc gr0_implies_Suc gr_implies_not0 less_Suc_induct less_irrefl_nat nat_less_induct infinite_descent nat.exhaust_disc infinite_descent0 linorder_neqE_nat strict_inc_induct less_Suc_eq_0_disj less_nat_zero_code not_less_less_Suc_eq infinite_descent_measure infinite_descent0_measure Euclidean_Division.div_eq_0_iff nat_mult_eq_cancel1 nat_mult_less_cancel1 less_mult_imp_div_less nat_less_le less_imp_le_nat le_eq_less_or_eq less_or_eq_imp_le le_neq_implies_less less_mono_imp_le_mono add_lessD1 add_less_mono not_add_less1 not_add_less2 add_less_mono1 trans_less_add1 trans_less_add2 less_add_eq_less diff_less_mono2 less_imp_diff_less nat_power_less_imp_less div_if dividend_less_times_div dividend_less_div_times split_div zero_power le_div_geq div_nat_eqI split_div' Suc_leI Suc_le_eq dec_induct inc_induct Suc_le_lessD le_less_Suc_eq less_Suc_eq_le less_eq_Suc_le le_imp_less_Suc less_imp_Suc_add less_iff_Suc_add less_add_Suc2 less_add_Suc1 Suc_diff_Suc diff_Suc_less diff_less_Suc mono_nat_linear_lb Suc_mult_less_cancel1 n_less_n_mult_m n_less_m_mult_n one_less_mult diff_less_mono less_diff_iff nat_mult_le_cancel1 add_diff_inverse_nat less_diff_conv nat_diff_split nat_diff_split_asm div_2_gt_zero Suc_n_div_2_gt_zero power_eq_imp_eq_base power_eq_iff_eq_base pos2 linordered_field_no_lb linordered_field_no_ub real_archimedian_rdiv_eq_0 realpow_pos_nth realpow_pos_nth_unique less_diff_conv2 div_le_mono div_le_dividend div_mult2_eq less_2_cases nat_less_add_iff2 nat_less_add_iff1 times_divide_times_eq divide_divide_times_eq add_divide_distrib diff_divide_distrib Suc_div_le_mono times_div_less_eq_dividend div_times_less_eq_dividend lemma_MVT divide_right_mono_neg divide_nonpos_nonpos divide_nonpos_nonneg divide_nonneg_nonpos divide_nonneg_nonneg zero_le_divide_iff divide_right_mono divide_le_0_iff divide_strict_right_mono_neg divide_strict_right_mono zero_less_divide_iff divide_less_cancel divide_less_0_iff divide_pos_pos
"mash": Including 1000 relevant facts: power2_sum power2_eq_square one_power2 Groups.mult_ac(2) power_add four_x_squared real_sqrt_pow2 semiring_normalization_rules(8) linorder_not_le semigroup.intro semiring_normalization_rules(4) add_0_right Groups.mult_ac(1) mult_2 Groups.mult_ac(3) add_0_left Groups.add_ac(2) bounded_bilinear_def mult_minus_right add_sign_intros(4) linorder_not_less ln_div real_sqrt_sum_squares_triangle_ineq abel_semigroup.intro abel_semigroup_axioms.intro distrib_left linorder_linear numeral_code(1) dvd_refl abel_semigroup.left_commute zero_le_power_eq_numeral order_less_irrefl exp_bound mult_1s(1) mult_zero_left mult.left_neutral abel_semigroup.commute One_nat_def mult_compare_simps(14) abs_of_nonneg power2_le_imp_le sqrt_sum_squares_le_sum zero_less_numeral mult_sign_intros(1) L2_set_mult_ineq_lemma mult_2_right arith_simps(10) le_add_same_cancel1 comm_semiring_class.distrib comm_monoid_mult_class.mult_1 semiring_1_class.of_nat_simps(2) arctan_add arctan_double times_divide_eq_left rel_simps(27) rel_simps(76) add_mono_thms_linordered_semiring(1) times_divide_eq_right dbl_simps(5) powr_mult dbl_def powr_add real_sqrt_sum_squares_ge1 real_sqrt_abs mult_minus_left arith_simps(16) arith_simps(52) add_uminus_conv_diff power_one arsinh_real_def add_mono_thms_linordered_field(5) sincos_total_2pi_le arsinh_real_aux add_Suc_right powr_half_sqrt sincos_total_2pi arith_simps(12) real_norm_def arctan_half sin_integer_2pi id_apply Groups.add_ac(3) real_exp_bound_lemma diff_minus_eq_add exp_lower_taylor_quadratic monoseq_arctan_series semiring_1_class.of_nat_simps(1) someI_ex real_sqrt_sum_squares_mult_squared_eq cos_one_2pi_int real_sqrt_sum_squares_eq_cancel2 add_diff_cancel_left' sqrt_def real_sqrt_sum_squares_eq_cancel cos_integer_2pi real_sqrt_sum_squares_mult_ge_zero summable_arctan_series zeroseq_arctan_series sin_two_pi arctan_series abs_ln_one_plus_x_minus_x_bound cos_double_less_one abs_exp_cancel exp_bound_lemma inverse_eq_divide real_sqrt_ge_0_iff zero_le_one real_sqrt_ge_abs1 real_sqrt_ge_abs2 real_sqrt_sum_squares_ge2 add.inverse_inverse mult.right_neutral order.trans of_nat_numeral bounded_bilinear.pos_bounded abs_ln_one_plus_x_minus_x_bound_nonpos power_eq_0_iff sin_times_pi_eq_0 rel_simps(28) complex_norm cancel_comm_monoid_add_class.diff_cancel le_divide_eq_numeral1(1) bounded_bilinear.bounded cos_arctan of_real_eq_id cos_x_y_le_one mult_eq_0_iff mult_zero_right DERIV_arctan_series power.simps(2) add_mono_thms_linordered_field(1) sqrt_sum_squares_le_sum_abs Ints_mult sincos_total_pi add_diff_eq sin_arctan order_less_imp_le cos_arccos_lemma1 of_nat_power divide_inverse Ints_cases sincos_total_pi_half sqrt_sum_squares_half_less complex_inverse of_nat_eq_0_iff real_sqrt_sum_squares_less div_by_1 DERIV_arctan DERIV_cong log_def arcosh_real_def tanh_ln_real log_mult powr_one_gt_zero_iff arsinh_def sin_arccos_lemma1 arith_special(3) sin_arccos_abs zero_less_one divide_divide_eq_right sin_paired summable_Leibniz(1) arsinh_real_has_field_derivative ln_one_plus_pos_lower_bound nat_induct abs_ln_one_plus_x_minus_x_bound_nonneg divide_self_if power_zero_numeral arith_geo_mean_sqrt zero_le_mult_iff cosh_ln_real order_refl DERIV_const DERIV_fun_pow monoid_axioms.intro ln_mult diff_zero not_one_le_zero power.simps(1) ab_group_add_class.ab_diff_conv_add_uminus distrib_right monoid.intro divide_divide_eq_left times_complex.sel(2) tan_def bounded_bilinear.intro power2_abs DERIV_powr norm_ge_zero linear_plus_1_le_power DERIV_power less_eq_real_def mult_left_mono times_complex.sel(1) eq_divide_eq real_sqrt_eq_0_iff sum_power2_ge_zero ordered_ring_class.le_add_iff1 arith_simps(1) log_of_power_eq nonzero_mult_div_cancel_right semiring_norm(76) combine_common_factor vector_space_assms(3) abs_ge_zero monoid.left_neutral add_cancel_left_left add_cancel_left_right tan_arctan DERIV_fun_powr ln_one_minus_pos_lower_bound order_antisym_conv le_add_same_cancel2 complex_eq_iff of_nat_mult atMost_iff max.cobounded2 real_sqrt_unique power2_minus bounded_bilinear.nonneg_bounded of_int_numeral real_sqrt_four add_divide_eq_if_simps(1) ext Maclaurin_sin_expansion2 realpow_square_minus_le sinh_ln_real zero_compare_simps(12) real_less_rsqrt add_sign_intros(1) UNIV_I power2_diff add_left_cancel square_diff_one_factored split_mult_pos_le Maclaurin_sin_expansion cmod_def real_le_rsqrt cos_arccos_abs real_scaleR_def eq_divide_eq_numeral1(1) add_mono_thms_linordered_field(4) sqrt_le_D vector_space_assms(2) ln_sqrt not_sum_power2_lt_zero ln_eq_zero_iff mult_1s(2) one_less_numeral_iff less_add_iff1 Maclaurin_sin_expansion4 add.inverse_neutral Re_divide real_le_lsqrt vector_space_assms(4) mult_compare_simps(13) Maclaurin_minus_cos_expansion Maclaurin_sin_expansion3 divide_eq_eq_numeral1(1) Maclaurin_cos_expansion distrib_right_numeral Maclaurin_cos_expansion2 of_nat_sum cmod_power2 diff_ge_0_iff_ge arith_geo_mean plus_nat.simps(2) monoid.right_neutral arith_simps(45) sqrt_ge_absD real_less_lsqrt add_mono_thms_linordered_field(3) powr_diff real_average_minus_second of_nat_eq_iff inverse_complex.sel(1) nat.simps(3) numeral.simps(3) times_nat.simps(2) real_average_minus_first sin_arccos cos_periodic sin_periodic inverse_complex.sel(2) semigroup.assoc arith_simps(58) tan_periodic uminus_add_conv_diff add_divide_eq_if_simps(4) sums_if cos_arcsin one_less_log_cancel_iff Im_divide log_less_one_cancel_iff divide_minus_left of_nat_add pos2 binomial Im_power2 power_divide cot_periodic add_le_cancel_left cos_add powr_numeral DERIV_const_average le_0_eq real_minus_mult_self_le Suc_leI zero_order(1) cis_mult order_le_less numeral.simps(2) complex_eq_0 zero_less_diff lemma_termdiff3 mult_1s(3) tanh_def mult_Suc_right one_le_power binomial_r_part_sum of_int_minus abs_divide Parity.ring_1_class.power_minus_even complex_mult_cnj power_minus_odd DERIV_arcsin arcosh_def complex_neq_0 numeral_times_minus_swap left_add_twice rcis_def BitM.simps(1) left_diff_distrib_numeral Complex_divide num.rec(1) minus_mult_commute of_real_mult DERIV_arccos minus_mult_right power_mult_distrib add_divide_distrib eq_add_iff2 sum_squares_bound complex_unit_circle complex_surj artanh_real_has_field_derivative arcosh_real_has_field_derivative neg_0_less_iff_less inverse_numeral_1 rcis_mult arith_simps(19) nat_numeral cos_ge_zero divide_le_eq exp_first_two_terms real_sqrt_le_iff arith_simps(55) power2_eq_imp_eq real_root_pos_unique sin_add sin_2npi cos_2npi cos_double arcsin of_int_eq_iff add_diff_cancel_left add_frac_eq divide_complex_def cos_one_2pi diff_0 cos_pi sin_pi cos_tan inverse_complex.ctr ex_power_ivl2 mult_0_right sin_tan exp_ln sum_power2_eq_zero_iff real_sqrt_less_iff zero_neq_one of_real_eq_0_iff cis.sel(2) cis.sel(1) sin_int_2pin floor_log_nat_eq_if cos_pi_half sin_pi_half cos_int_2pin nonzero_mult_div_cancel_left ex_power_ivl1 vector_space_assms(1) rel_fun_eq floor_log_nat_eq_powr_iff of_nat_id cos_paired cos_arccos zero_complex.sel(1) zero_complex.sel(2) sin_ge_zero is_equality_def is_equality_eq sum.cong atLeastAtMost_iff transfer_start sin_arcsin Rel_def ceiling_log_nat_eq_if exp_two_pi_i exp_two_pi_i' sin_cos_squared_add2 arccos_cos_eq_abs_2pi bij_betw_roots_unity add_diff_cancel_right' ceiling_log_nat_eq_powr_iff arccos_bounded pi_series pi_neq_zero comm_monoid_add_class.add_0 Rel_abs arctan_one power_even_eq eventually_True even_diff_nat Rel_app cos_minus of_real_power eq_diff_eq powr_neg_numeral choose_square_sum Real_Vector_Spaces.linear_def sin_minus sum_split_even_odd linorder_neqE_linordered_idom eq_add_iff1 neq0_conv abs_le_iff complex_eqI vector_space.intro powr_realpow sin_double square_le_1 has_derivative_arctan diff_Suc_Suc inverse_eq_divide_numeral cos_npi cos_limit_1 eq_diff_eq' vector_space.vector_space_assms(2) real_add_less_0_iff real_0_less_add_iff power_mult sin_bound_lemma le0 Suc_le_mono sin_squared_eq of_nat_eq_id vector_space.vector_space_assms(3) Suc_eq_plus1 odd_real_root_unique diff_eq_eq at_right_to_0 sin_expansion_lemma real_add_le_0_iff real_0_le_add_iff gbinomial_r_part_sum power2_i imageE has_real_derivative_pos_inc_right power_odd_eq add_divide_eq_iff tan_periodic_n right_diff_distrib' odd_real_root_power_cancel transfer_implies_transfer(1) module.intro cos_squared_eq Real.positive_add central_binomial_lower_bound cos_diff_limit_1 plus_inverse_ge_2 cos_expansion_lemma complex_add DERIV_pos_inc_right of_real_add summable_Leibniz(5) num_eq_iff cnj_add_mult_eq_Re DERIV_compose_FDERIV neg_less_iff_less subsetI vector_space.vector_space_assms(4) sum_power2_gt_zero_iff dvdE equalityI vector_space.vector_space_assms(1) linorder_neqE_nat DERIV_neg_dec_right minus_add zero_less_Suc module_hom_eq_linear empty_iff order_trans pred_numeral_simps(2) oddE le_less_trans cosh_def cosh_double sin_npi evenE real.right_total num.rec(2) fact_double even_add add_strict_mono Domainp_pcr_real diff_add_cancel arccos_1 neg_0_le_iff_le cos_le_one zmod_numeral_Bit1 summable_Leibniz'(5) pos_zdiv_mult_2 max.bounded_iff complex_of_real_add_Complex sin_periodic_pi2 Complex_add_complex_of_real two_realpow_ge_one right_diff_distrib complex_mod_mult_cnj cos_ge_minus_one pochhammer_double machin_Euler cos_zero plus_real.transfer nat_of_num_add scaleR_left.add dist_triangle_less_add nat.simps(1) mult_div_mod_eq complex_norm_square Real.positive.transfer eventually_at_right_to_0 of_int_simps(2) Ints_of_int of_real_def tan_periodic_int eventually_filtermap cos_periodic_pi2 sqrt_add_le_add_sqrt arith_series_nat log2_of_power_eq real_sqrt_pow2_iff pos_zmod_mult_2 filtermap_filtermap summable_Leibniz'(4) additive.intro powr_int power3_eq_cube dvd_triv_left numerals(2) sum_power2_le_zero_iff tanh_real_altdef less_le_trans filterlim_at_right_to_0 neg_zdiv_mult_2 cosh_square_eq additive.add filterlim_def tendsto_rabs_zero_iff continuous_on_arccos' real_sqrt_power_even minus_diff_eq times_nat.simps(1) sin_cos_squared_add Maclaurin_lemma gbinomial_partial_sum_poly real_inv_sqrt_pow2 rel_simps(70) ln_series sums_alternating_upper_lower power_add_numeral2 of_real_1 num.rec(3) add_mono_thms_linordered_semiring(3) i_even_power power2_nat_le_eq_le power2_csqrt power2_nat_le_imp_le diff_gt_0_iff_gt arith_simps(2) Groups.add_ac(1) cos_two_pi of_real_numeral power_add_numeral neg_less_eq_nonneg integer_of_num_def sin_cos_npi prod.simps(2) choose_even_sum Suc_double_not_eq_double ab_group_add_class.ab_left_minus choose_odd_sum double_not_eq_Suc_double binomial_ring lemma_termdiff2 numeral_3_eq_3 one_neq_zero integer_of_char_code semiring_normalization_rules(29) parity_induct summable_Leibniz(3) semiring_normalization_rules(26) summable_Leibniz(2) complex_div_cnj nat_of_num_mult gbinomial_partial_sum_poly_xpos gbinomial_negated_upper sqrt_even_pow2 dvd_add_left_iff cosh_add choose_row_sum length_subseqs divmod_step_nat_def binomial_le_pow2 DeMoivre binomial_symmetric sum_power_add tendsto_exp_limit_sequentially tan_sec card_Pow complex_add_cnj push_bit_of_Suc_0 le_log2_of_power square_fact_le_2_fact less_log2_of_power vandermonde zero_power2 tendsto_const neg_zmod_mult_2 of_int_simps(3) push_bit_eq_mult power_minus1_even exp_double abs_1 sin_cos_squared_add3 lessThan_iff powr_mult_base ln_powr Re_power2 left_add_mult_distrib DeMoivre2 Re_Reals_divide exp_le_cancel_iff m2pi_less_pi sin_cos_sqrt binomial_gbinomial minus_add_distrib nat_distrib(1) zero_less_mult_iff zero_eq_power2 powr_gt_zero tan_periodic_nat log2_of_power_less continuous_on_tendsto_compose diff_diff_add power2_eq_1_iff csqrt_unique ln_exp log_add_eq_powr odd_two_times_div_two_succ pos_eucl_rel_int_mult_2 prod.sel(2) semiring_normalization_rules(36) prod.sel(1) i_squared power_numeral_odd csqrt_square power_minus1_odd Power.ring_1_class.power_minus_even double_arith_series add_log_eq_powr cos_2pi_minus log2_of_power_le sum_power2 cot_def division_ring_divide_zero choose_linear_sum exp_inj_iff arith_simps(9) fact_0 divmod_step_int_def atLeastLessThan_iff right_minus_eq log_powr_cancel tan_periodic_pi inverse_mult_distrib sum.empty diffs_def cos_pi_eq_zero less_log_of_power binomial_maximum' sin_2pi_minus zdvd_period DERIV_ident linorder_cases pi_def Im_Reals_divide not_mod_2_eq_0_eq_1 log_divide le_log_of_power atLeastLessThan_empty lessI has_real_derivative_neg_dec_right integer_of_char_def summable_Leibniz(4) eq_numeral_Suc odd_two_times_div_two_nat divmod_step_integer_def zmod_numeral_Bit0 binomial_mono real_of_nat_eq_numeral_power_cancel_iff arith_simps(15) group_axioms.intro sin_lt_zero binomial_strict_mono norm_diff_triangle_ineq even_Suc norm_diff_triangle_less complex_cnj_zero_iff binomial_strict_antimono complex_is_Real_iff log_of_power_less exp_minus divmod_int_unique(2) divmod_int_unique(1) eucl_rel_int mult_numeral_left(1) left_minus minus_power_mult_self log_of_power_le sin_le_zero div_mult_mod_eq dvd_mult complex_mod_cnj numeral_pow take_bit_numeral_bit1 group.intro neg_eucl_rel_int_mult_2 le_real_sqrt_sumsq char.sel(8) zero_order(3) Nat.add_diff_assoc2 cos_plus_cos odd_Suc_minus_one summable_Leibniz'(3) mult_divide_mult_cancel_left_if power2_commute add_diff_cancel norm_diff_triangle_le scaleR_half_double odd_real_root_pow add_le_mono cos_npi2 comm_monoid_axioms.intro char.sel(7) add_numeral_left char.sel(6) sinh_def comm_monoid_set.intro comm_monoid.intro char.sel(5) char.sel(4) power_half_series char.sel(3) sinh_double char.sel(2) neg_equal_iff_equal char.sel(1) numeral_code(3) power_numeral_even tendsto_minus norm_triangle_ineq exp_not_eq_zero add_neg_numeral_left(3) binomial_Suc_Suc complex_diff_cnj DERIV_minus ln_unique binomial_maximum norm_mult double_gauss_sum empty_subsetI odd_iff_mod_2_eq_one filtermap_at_right_shift arith_series norm_triangle_mono int_of_integer_numeral tendsto_ident_at summable_Leibniz'(2) fact_Suc complex_mult dvd_eq_mod_eq_0 Int_iff Diff_iff pi_gt_zero power2_eq_iff binomial_n_0 choose_mult_lemma complex_unimodular_polar zero_le_power drop_bit_eq_div Maclaurin_exp_le real_root_mult double_gauss_sum_from_Suc_0 arith_simps(53) power_minus_Bit0 DERIV_chain2 even_iff_mod_2_eq_zero of_char_Char power_inverse add_eq_0_iff2 diff_diff_eq2 mult_numeral_left(3) IntE left_diff_distrib power_Suc_0 of_int_simps(1) is_num_normalize(2) LIMSEQ_inverse_real_of_nat_add_minus filterlim_pow_at_bot_odd numeral_nat(3) binomial_0_Suc cos_double_cos one_le_mult_iff pos_add_strict mult_numeral_left(4) Domainp_forall_transfer sin_npi2 le_neq_trans mult_numeral_left(2) Maclaurin_exp_lt real_root_pow_pos2 Un_iff cos_double_sin finite_lessThan push_bit_of_1 take_bit_Suc integer_eq_iff finite_Un scaleR_conv_of_real nat_one_le_power zero_less_abs_iff binomial_n_n norm_of_real module.scale_left_distrib le_Suc_numeral take_bit_eq_mod dist_triangle_lt exp_add_commuting log_powr Re_complex_of_real machin zero_integer.rep_eq real_differentiable_def Maclaurin_all_le_objl minus_real_def Im_complex_of_real scaleR_eq_0_iff polar_Ex powr_def eventually_rev_mp Maclaurin_all_le norm_add_less cos_treble_cos split_def one_div_2_pow_eq real_add_minus_iff cis_zero int_of_integer_code eventuallyI cos_n_Re_cis_pow_n sin_n_Im_cis_pow_n integer_of_int_eq_of_int mult_scaleR_right filterlim_pow_at_bot_even Maclaurin_all_lt one_integer.rep_eq Maclaurin_bi_le has_derivative_tan less_Suc_numeral exp_ge_add_one_self sgn_power_injE numeral_eq_Suc divide_eq_0_iff sin_periodic_pi mult_less_cancel_left_pos tan_double int_of_integer_of_int cos_periodic_pi square_norm_one reals_Archimedean3 real_mult_le_cancel_iff2 integer_of_int_code power2_eq_iff_nonneg vector_space_axioms right_inverse real_bounded_linear add_le_less_mono power_minus one_mod_2_pow_eq less_induct sin_pi_minus less_add_iff2 of_char_def filterlim_pow_at_top card_lessThan take_bit_eq_0_iff split_root mult_sign_intros(5) real_linearD norm_minus_cancel pochhammer_times_pochhammer_half sin_gt_zero real_mult_less_iff1 diff_0_right real_sqrt_abs2 real_archimedian_rdiv_eq_0 root_0 gbinomial_sum_nat_pow2 plus_integer.rep_eq filterlim_uminus_at_bot distrib_left_numeral span_raw_def times_integer.rep_eq uminus_integer.rep_eq Real.positive_mult sum_op_ivl_Suc norm_one dependent_raw_def square_eq_1_iff real_sqrt_mult not_real_square_gt_zero divmod_cancel(2) divide_real_def less_trans numeral_powr_numeral_real div_less_dividend ball_UNIV sum_constant scaleR_right.zero div_integer_code mod_integer_code Diff_empty neg_le_0_iff_le power2_less_imp_less real_divide_square_eq numeral_sqr divide_integer.rep_eq ln_realpow realpow_pos_nth exp_series_add_commuting modulo_integer.rep_eq rel_simps(25) of_nat_less_numeral_power_cancel_iff of_nat_le_numeral_power_cancel_iff dist_norm numeral_power_le_of_nat_cancel_iff termdiffs_aux numeral_power_less_of_nat_cancel_iff filterlim_compose real_mult_le_cancel_iff1 binomial_code linordered_comm_semiring_strict_class.comm_mult_strict_left_mono sum_distrib_left zero_diff card_UNION realpow_pos_nth2 zero_le_even_power' summable_sums lemma_termdiff1 realpow_pos_nth_unique monoseq_realpow power_one_right exp_ge_one_plus_x_over_n_power_n convergent_realpow take_bit_numeral_bit0 push_bit_Suc even_two_times_div_two filterlim_uminus_at_top has_derivative_arcsin prod_constant real_sqrt_power push_bit_double numeral_power_eq_nat_cancel_iff divmod_digit_1(1) nat_eq_numeral_power_cancel_iff dvd_mult_div_cancel square_eq_iff scaleR_minus_right 
"vampire" slice #1 with 500 facts for 19.9 s... 
"z3" slice 1 with 350 facts for 19.9 s 
"cvc4" slice 1 with 400 facts for 19.9 s 
The Vampire prover is not activated; to activate it, set the Isabelle system option "vampire_noncommercial" to
"yes" (e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General)