proposition: Lemma trunc_sqrt: forall n, Zfloor (sqrt (IZR n)) = Z.sqrt n.
proof: Proof. intros [| p | p ]; [now rewrite sqrt_0, Zfloor_IZR | |]. - symmetry. apply Z.sqrt_unique. unfold Z.succ. rewrite <-(Zfloor_IZR (Z.pos p)), <-(sqrt_def (IZR (Z.pos p))) at 3 4 by now apply IZR_le. rewrite Zfloor_add. split; [apply Zfloor_mul, sqrt_ge_0 |]. apply (Z.le_lt_trans _ (Z.pos p)). + apply le_IZR. rewrite <-(sqrt_def (IZR (Z.pos p))) at 3 by now apply IZR_le. apply Zfloor_lb. + apply lt_IZR. rewrite <-(sqrt_def (IZR (Z.pos p))) at 1 by now apply IZR_le. rewrite mult_IZR. apply Rmult_lt_compat; [apply sqrt_ge_0 | apply sqrt_ge_0 | rewrite <-Zfloor_add; rewrite plus_IZR; apply Zfloor_ub..]. - rewrite sqrt_neg; [| now apply IZR_le]. now rewrite Zfloor_IZR. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)