[STATEMENT]
lemma mult_ge1_powers [mono_intros]:
  assumes "a \<ge> (1::'a::linordered_idom)"
  shows "1 \<le> a * a" "1 \<le> a * a * a" "1 \<le> a * a * a * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> a * a &&& (1::'a) \<le> a * a * a &&& (1::'a) \<le> a * a * a * a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(1::'a) \<le> a

goal (1 subgoal):
 1. (1::'a) \<le> a * a &&& (1::'a) \<le> a * a * a &&& (1::'a) \<le> a * a * a * a
[PROOF STEP]
by (meson assms dual_order.trans mult_ge1_mono(1) zero_le_one)+