proposition: Theorem div_Rdiv : forall n m : nat, 0 < m -> (INR (div n m) <= INR n / INR m)%R.
proof: Proof. intros n m H; apply Rmult_le_reg_l with (r := INR m); auto with real. replace (INR m * (INR n / INR m))%R with (INR n). rewrite <- mult_INR; apply le_INR; auto with arith. apply div_le; auto. unfold Rdiv in |- *. replace (INR m * (INR n * / INR m))%R with (INR n * (INR m * / INR m))%R; [ rewrite Rinv_r | ring ]; auto with real. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)