proposition: Lemma a_familiar_simple_inequality : forall m : nat, 4 <= m -> (Two [/]ThreeNZ)[^]m[<](([1]:R1)[/] nring (S m)[//]nringS_ap_zero _ m).
proof: Proof. intros. induction m as [| m Hrecm]. apply False_rect. generalize H. change (~ 4 <= 0) in |- *. apply Nat.nle_succ_0. case (le_lt_eq_dec 4 (S m) H). intro. apply less_transitive_unfolded with (y := Two [/]ThreeNZ[*](([1]:R1)[/] nring (S m)[//]nringS_ap_zero _ m)). astepl (((Two:R1) [/]ThreeNZ)[^]m[*]Two [/]ThreeNZ). astepl ((Two:R1) [/]ThreeNZ[*](Two [/]ThreeNZ)[^]m). apply mult_resp_less_lft. apply Hrecm. apply Nat.lt_succ_r. assumption. apply div_resp_pos. apply pos_three. apply pos_two. apply mult_cancel_less with (z := (Three:R1)[*]nring (S m)[*]nring (S (S m))). apply mult_resp_pos. apply mult_resp_pos. apply pos_three. apply pos_nring_S. apply pos_nring_S. rstepl ((Two:R1)[*]nring (S (S m))). rstepr ((Three:R1)[*]nring (S m)). astepl ((Two:R1)[*](nring m[+]Two)). astepr ((Three:R1)[*](nring m[+][1])). apply plus_cancel_less with (z := [--]((Two:R1)[*]nring m[+]Three)). rstepl ([1]:R1). rstepr (nring (R:=R1) m). astepl (nring (R:=R1) 1). apply nring_less. apply Nat.lt_trans with (m := 3). constructor. constructor. apply Nat.succ_lt_mono. assumption. simpl in |- *. algebra. apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. simpl in |- *. rational. intro H0. rewrite <- H0. apply mult_cancel_less with (z := nring (R:=R1) 5[*]Three[^]4). apply mult_resp_pos. apply pos_nring_S. rstepr (Three[^]2[*](Three[^]2:R1)). apply mult_resp_pos. apply pos_square. apply nringS_ap_zero. apply pos_square. apply nringS_ap_zero. rstepl (Two[^]4[*]nring (R:=R1) 5). rstepr (Three[^]4:R1). rstepl (nring (R:=R1) 80). rstepr (nring (R:=R1) 81). apply nring_less. constructor. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon