proposition: Lemma PrimInt63_opp_inj : forall x y, (- x)%uint63 = (- y)%uint63 -> x = y.
proof: Proof. intros x y H. rewrite <-(PrimInt63_opp_involutive x), <-(PrimInt63_opp_involutive y). now apply f_equal. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)