proposition: Lemma addc_spec x y : [+| x +c y |] = φ x + φ y .
proof: Proof. rewrite addc_def_spec; unfold addc_def, interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case ltbP; rewrite add_spec. - case (Z_lt_ge_dec (φ x + φ y ) wB). + intros k; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y - wB)); lia. - case (Z_lt_ge_dec (φ x + φ y ) wB). + intros k; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 (φ x + φ y - wB)); lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63