proposition: Lemma subc_spec x y : [-| x -c y |] = φ x - φ y .
proof: Proof. rewrite subc_def_spec; unfold subc_def; unfold interp_carry. pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). case lebP. - intros hle; rewrite sub_spec, Z.mod_small; lia. - intros hgt; rewrite sub_spec, <- (Zmod_unique _ wB (-1) (φ x - φ y + wB)); lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63