proposition: Lemma RfactN_fact2N_factk : forall N k:nat, (k <= 2 * N)%nat -> Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).
proof: Proof. assert (forall (n:nat), 0 <= (if eq_nat_dec n 0 then 1 else INR n)). { intros; case (eq_nat_dec n 0); auto with real. } assert (forall (n:nat), (0 < n)%nat -> (if eq_nat_dec n 0 then 1 else INR n) = INR n). { intros n; case (eq_nat_dec n 0); auto with real. intros; absurd (0 < n)%nat; lia. } intros; unfold Rsqr; repeat rewrite fact_prodSO. assert (H2:(k=N)%nat \/ (k < N)%nat \/ (N < k)%nat) by lia. elim H2; intro H3. { rewrite H3; replace (2*N-N)%nat with N by lia;right; ring. } case H3; intro; clear H2 H3. + rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N). 2:{ lia. } rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply prod_SO_pos; intros; auto. } replace (2 * N - k - N-1)%nat with (N - k-1)%nat by lia. rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N k). 2:{ lia. } apply Rmult_le_compat_l. * apply prod_SO_pos; intros; auto. * apply prod_SO_Rle; intros; split; auto. rewrite H0. -- rewrite H0. ++ apply le_INR; lia. ++ lia. -- lia. + rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) k)); rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) k N). 2:{ lia. } rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply prod_SO_pos; intros; auto. } rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N (2 * N - k)). 2:{ lia. } apply Rmult_le_compat_l. { apply prod_SO_pos; intros; auto. } replace (N - (2 * N - k)-1)%nat with (k - N-1)%nat. 2:{ lia. } apply prod_SO_Rle; intros; split; auto. rewrite H0. 2:{ lia. } rewrite H0. 2:{ lia. } apply le_INR; lia. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia