[STATEMENT]
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n \<Longrightarrow> monoseq X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. X (Suc n) \<le> X n \<Longrightarrow> monoseq X
[PROOF STEP]
by (simp add: monoseq_Suc)