proposition: Lemma sub_pow2 : forall x k m, (0 <= k < m)%Z -> (0<= x < 2^m)%Z -> (x - x mod 2 ^ (k+1) + 2^k < 2^ m )%Z.
proof: Proof. intros. assert (2 ^(k +1) = 2 * 2^k)%Z. { rewrite Z.pow_add_r; lia. } rewrite H1. clear H1. assert (exists n, Z.of_nat n = m). { exists (Z.to_nat m). lia. } destruct H1 as (m' & EQ). subst. revert x k H0 H. induction m'. - intros. change (2^ Z.of_nat 0)%Z with 1%Z in *. assert (x = 0)%Z by lia. subst. lia. - intros. replace (Z.of_nat (S m'))%Z with (1 + Z.of_nat m')%Z in * by lia. assert (DB : (0 <= x / 2 < 2^ Z.of_nat m')%Z). { rewrite Z.pow_add_r in H0 by lia. lia. } assert (k = 0 \/ 0<= k-1 < Z.of_nat m')%Z by lia. destruct H1. + subst. change (2 * 2^0)%Z with 2%Z. rewrite Z.pow_add_r in * by lia. lia. + specialize (IHm' (x / 2)%Z _ DB H1). rewrite Z.pow_add_r by lia. assert (2 * 2^ (k-1) = 2 ^k)%Z. { change 2%Z with (2^1)%Z at 1. rewrite <- Z.pow_add_r by lia. f_equal. lia. } rewrite H2 in IHm'. assert (2^0 <= 2 ^ k)%Z. { apply Z.pow_le_mono_r; lia. } assert (2 * (x / 2 - (x / 2) mod 2 ^ k + 2 ^ (k - 1)) + 1 < 2 * 2 ^ Z.of_nat m')%Z by lia. eapply Z.le_lt_trans ; eauto. ring_simplify. rewrite H2. cut (x - x mod (2 * 2 ^ k) <= 2 * (x / 2) - 2 * ((x / 2) mod 2 ^ k) + 1)%Z. lia. clear - H3. zify. rewrite H5 by lia. rewrite H10 by lia. assert (q1 = q0) by nia. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR