proposition: Lemma holes_in_powers : forall n z : nat, two_power n < z -> z < two_power (S n) -> forall p : nat, z <> two_power p.
proof: Proof. unfold not in |- *; intros. cut (n < p). intro. cut (p < S n). intro. case (lt_not_lt n p); auto with arith. apply two_power_monoR. elim H1; auto with arith. apply two_power_monoR. elim H1; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Le_lt_compl