proposition: Lemma floor_log2 : forall n : nat, 0 < n -> {l : nat | two_power l <= n /\ n < two_power (S l)}.
proof: Proof. refine (fun n _ => match log2 n _ with | existS l b => exist _ l _ end). auto with arith. elim b; intro. rewrite a; split; auto with arith. elim b0; auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl shift Compare_dec two_power