proposition: Lemma cmod_cmod : forall a b, (0 < b)%Z -> (a cmod b)%Z = Sint63.cmod a b.
proof: Proof. intros a b H. unfold Zcmod, Sint63.cmod. now rewrite Zquot.Zquot_Zdiv_pos; [| lia |]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)