proposition: Lemma shiftr_eq_0 : forall a n, log2 a < n -> a >> n == 0.
proof: Proof. intros a n H. rewrite shiftr_eq_0_iff. destruct (eq_0_gt_0_cases a) as [EQ|LT]. - now left. - right; now split. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog