proposition: Lemma shiftr_eq_0 : forall a n, 0<=a -> log2 a < n -> a >> n == 0.
proof: Proof. intros a n Ha H. apply shiftr_eq_0_iff. le_elim Ha. - right. now split. - now left. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog