proposition: Lemma cmod_bounded : forall a b, (0 < b)%Z -> (- (b / 2) <= a cmod b <= b - b / 2 - 1)%Z.
proof: Proof. intros a b H0. rewrite cmod_cmod by assumption. generalize (Z.mod_pos_bound (a + b / 2) b H0). unfold Sint63.cmod. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)