proposition: Theorem sqr_Rsqrt : forall n : nat, (INR (sqr n) <= sqrt (INR n))%R.
proof: Proof. intros n; apply Rle_square; auto with real. apply sqrt_positivity; replace 0%R with (INR 0); auto with real arith. rewrite <- sqrt_mult; try rewrite sqrt_square; auto with real. rewrite <- mult_INR; apply le_INR. apply sqr_le. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)