proposition: Lemma PrimInt63_opp_involutive : forall x, (- - x)%uint63 = x.
proof: Proof. intros x. apply Uint63.to_Z_inj. now rewrite 2Uint63.opp_spec, <-Z.sub_0_l, Zdiv.Zminus_mod_idemp_r, Z.sub_0_l, Z.opp_involutive, Z.mod_small; [| apply Uint63.to_Z_bounded]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)