proposition: Lemma addmuldiv_spec x y p : φ p <= φ digits -> φ (addmuldiv p x y) = (φ x * (2 ^ φ p) + φ y / (2 ^ (φ digits - φ p))) mod wB.
proof: Proof. intros H. assert (Fp := to_Z_bounded p); assert (Fd := to_Z_bounded digits). rewrite addmuldiv_def_spec; unfold addmuldiv_def. case (bit_add_or (x << p) (y >> (digits - p))); intros HH _. rewrite <-HH, add_spec, lsl_spec, lsr_spec, Zplus_mod_idemp_l, sub_spec. - rewrite (fun x y => Zmod_small (x - y)); auto with zarith. - intros n; rewrite -> bit_lsl, bit_lsr. generalize (add_le_r (digits - p) n). case (_ ≤? _); try discriminate. rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1. case_eq (n <? p)%uint63; try discriminate. rewrite <- not_true_iff_false, ltb_spec; intros H2. case (_ ≤? _); try discriminate. intros _; rewrite bit_M; try discriminate. rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith. rewrite -> sub_spec, Zmod_small; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63