proposition: Lemma oppcarry_spec x : φ (oppcarry x) = wB - φ x - 1.
proof: Proof. unfold oppcarry; rewrite sub_spec. rewrite <- Zminus_plus_distr, Zplus_comm, Zminus_plus_distr. apply Zmod_small. generalize (to_Z_bounded x); auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63