proposition: Lemma ceiling_log2 : forall n : nat, one < n -> {l : nat | two_power (pred l) < n /\ n <= two_power l}.
proof: Proof. refine (fun n _ => match log2 n _ with | existS l b => match b with | left e => exist _ l _ | right a => exist _ (S l) _ end end). auto with arith. rewrite e; split. apply two_power_mono. cut (0 < l). generalize l; induction l as [| l Hrecl]; auto with arith. case (lt_or_Zero l); [ auto with arith | intro eg ]. absurd (one < n); [ rewrite e; rewrite eg; simpl in |- *; auto with arith | auto with arith ]. auto with arith. unfold pred in |- *; elim a; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl shift Compare_dec two_power