DκZ_le_two_rpow_100

lemma DκZ_le_two_rpow_100 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :    (D : ℝ≥0∞) ^ (-κ * Z) ≤ 2 ^ (-100 : ℝ) := by  rw [defaultD, Nat.cast_pow, ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul,    show ((2 : ℕ) : ℝ≥0∞) = 2 by rfl]  apply ENNReal.rpow_le_rpow_of_exponent_le one_le_two  rw [defaultκ, defaultZ, Nat.cast_pow, show ((2 : ℕ) : ℝ) = 2 by rfl, neg_mul,    show (2 : ℝ) ^ (12 * a) = 2 ^ (12 * a : ℝ) by norm_cast, mul_neg,    ← Real.rpow_add zero_lt_two, show (-10 * a + 12 * a : ℝ) = 2 * a by ring,    neg_le_neg_iff]  norm_cast  have : 1 ≤ 𝕔 := by linarith [seven_le_c]  have := four_le_a X  calc    _ ≤ 1 * 4 ^ 2 * 2 ^ (2 * 4) := by norm_num    _ ≤ _ := by      gcongr      norm_num