proposition: Lemma subcarryc_spec x y : [-| subcarryc x y |] = φ x - φ y - 1.
proof: Proof. rewrite subcarryc_def_spec; unfold subcarryc_def, interp_carry; fold (subcarry x y). pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case ltbP; rewrite subcarry_spec. - intros hlt; rewrite Zmod_small; lia. - intros hge; rewrite <- (Zmod_unique _ _ (-1) (φ x - φ y - 1 + wB)); lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63