proposition: Lemma abs_spec (x : int) : to_Z (abs x)%sint63 = cmod (Z.abs (to_Z x)) wB.
proof: Proof. unfold abs; case lebP. - intro leq0x; rewrite Z.abs_eq by easy. now rewrite <- of_Z_spec, of_to_Z. - intro nleq0x; rewrite Z.abs_neq. + now rewrite opp_spec. + now apply Z.lt_le_incl; rewrite <- Z.nle_gt. Qed.
imports: ZArith Uint63 Lia