[STATEMENT]
lemma bigtheta_const [landau_simp]:
  "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) \<in> \<Theta>(\<lambda>x. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NO_MATCH (1::'a) c; c \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> (\<lambda>x. c) \<in> \<Theta>(\<lambda>x. 1::'b)
[PROOF STEP]
by simp