proposition: Theorem pow_log_le : forall (x:nat)(h:log_domain x), two_power (log x h) <= x.
proof: Proof. intros x h; elim h using log_domain_ind2. simpl; auto with arith. intros p l Hle. lazy beta iota zeta delta [two_power log_domain_inv log]; fold log two_power. apply Nat.le_trans with (2 * S (div2 p)); auto with arith. generalize (double_div2_le (S (S p))); simpl;intro;lia. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9