proposition: Lemma Zfloor_add : forall x n, (Zfloor x + n)%Z = Zfloor (x + IZR n).
proof: Proof. intros x n. symmetry. apply Zfloor_imp. rewrite !plus_IZR. rewrite Rplus_assoc, (Rplus_comm _ 1), <-Rplus_assoc. split. - apply Rplus_le_compat_r, Zfloor_lb. - apply Rplus_lt_compat_r, Zfloor_ub. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)