proposition: Lemma pow_lt_compat : forall x y, 0 <= x -> x < y -> forall n, (1 <= n)%nat -> x ^ n < y ^ n.
proof: Proof. intros x y x_pos x_lt_y n n_lb. induction n. apply False_ind ; intuition (auto with arith); try lia. destruct n. simpl ; repeat (rewrite Rmult_1_r) ; assumption. assert (Hrew : forall a n, a ^ S (S n) = a * a ^ S n). intros a m ; simpl ; reflexivity. destruct x_pos as [x_pos | x_null]. do 2 rewrite Hrew. repeat (rewrite Hrew) ; apply Rmult_gt_0_lt_compat ; [apply pow_lt | | | apply IHn] ; intuition (auto with arith). apply Rlt_gt ; transitivity x ; assumption. rewrite Hrew, <- x_null, Rmult_0_l ; apply pow_lt ; apply Rle_lt_trans with x ; [right |] ; auto. Qed.
imports: Reals MyRIneq Fourier Lia Lra Rsequence_usual_facts