proposition: Lemma addcarryc_spec x y : [+| addcarryc x y |] = φ x + φ y + 1.
proof: Proof. rewrite addcarryc_def_spec; unfold addcarryc_def, interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case lebP; rewrite addcarry_spec. - case (Z_lt_ge_dec (φ x + φ y + 1) wB). + intros hlt; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y + 1 - wB)); lia. - case (Z_lt_ge_dec (φ x + φ y + 1) wB). + 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