proposition: Lemma shiftl_1_l : forall n, 1 << n == 2^n.
proof: Proof. intros n. destruct (le_gt_cases 0 n). - now rewrite shiftl_mul_pow2, mul_1_l. - rewrite shiftl_div_pow2, div_1_l, pow_neg_r; try order. apply pow_gt_1. + order'. + now apply opp_pos_neg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog