proposition: Lemma Zfloor_mul : forall x, 0 <= x -> Z.le (Zfloor x * Zfloor x)%Z (Zfloor (x * x)).
proof: Proof. intros x Hx. apply Zfloor_lub. rewrite mult_IZR. apply Rmult_le_compat. 3, 4: apply Zfloor_lb. all: apply IZR_le, Zlt_succ_le; unfold Z.succ; apply lt_IZR; rewrite plus_IZR; apply Rle_lt_trans with (1 := Hx), Zfloor_ub. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)