Sledgehammering... 
"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 
"cvc4" slice 1 with 400 facts for 19.9 s 
"vampire" slice #1 with 500 facts for 19.9 s... 
"z3" slice 1 with 350 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)