proposition: Lemma sub_sub_assoc : forall x y z, (x - (y - z) = x - y + z)%uint63.
proof: Proof. intros x y z. rewrite 3Sint63.sub_of_Z, Sint63.add_of_Z. apply Sint63.to_Z_inj. rewrite 4Sint63.of_Z_spec. rewrite <-4cmod_cmod by easy. unfold Zcmod at 1 3. unfold Z.sub. rewrite (Z.add_comm (Sint63.to_Z x)). rewrite Z.opp_eq_mul_m1. rewrite <-2Z.add_assoc, cmod_mul_add_mod; [| easy | now exists 1%Z]. rewrite cmod_add_mod; [| easy | now exists 1%Z]. apply f_equal with (f := fun n => (n mod wB + (- Z.quot wB 2))%Z). lia. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper