proposition: Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
proof: Proof. intros p x y H;destruct (Z_le_gt_dec 0 p). apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with y;auto with zarith. assert (0 < 2^p) by auto with zarith. rewrite <- (Z.mul_1_r y);apply Z.mul_le_mono_nonneg;auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia