proposition: Lemma shiftl_0_l : forall n, 0 << n == 0.
proof: Proof. intros n. destruct (le_ge_cases 0 n) as [H|H]. - rewrite shiftl_mul_pow2 by trivial. now nzsimpl. - rewrite shiftl_div_pow2 by trivial. rewrite <- opp_nonneg_nonpos in H. nzsimpl; order_nz. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog