proposition: Lemma div_pow2_bound :forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z.
proof: Proof. intros x y z HH HH1 HH2. split; auto with zarith. apply Z.le_lt_trans with (2 := HH2). apply Zdiv_le_upper_bound. auto with zarith. pattern x at 1; replace x with (x * 2 ^ 0). apply Z.mul_le_mono_nonneg_l; auto. apply Z.pow_le_mono_r; auto with zarith. rewrite Z.pow_0_r; ring. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen