proposition: Lemma limit_inv : forall (f:R -> R) (D:R -> Prop) (l x0:R), limit1_in f D l x0 -> l <> 0 -> limit1_in (fun x:R => / f x) D (/ l) x0.
proof: Proof. unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; elim (H (Rabs l / 2)). - intros delta1 H2; elim (H (eps * (Rsqr l / 2))). + intros delta2 H3; elim H2; elim H3; intros; exists (Rmin delta1 delta2); split. { unfold Rmin; case (Rle_dec delta1 delta2); intro; assumption. } intro; generalize (H5 x); clear H5; intro H5; generalize (H7 x); clear H7; intro H7; intro H10; elim H10; intros; cut (D x /\ Rabs (x - x0) < delta1). * cut (D x /\ Rabs (x - x0) < delta2). -- intros; generalize (H5 H11); clear H5; intro H5; generalize (H7 H12); clear H7; intro H7; generalize (Rabs_triang_inv l (f x)); intro; rewrite Rabs_minus_sym in H7; generalize (Rle_lt_trans (Rabs l - Rabs (f x)) (Rabs (l - f x)) (Rabs l / 2) H13 H7); intro; generalize (Rplus_lt_compat_l (Rabs (f x) - Rabs l / 2) (Rabs l - Rabs (f x)) (Rabs l / 2) H14); replace (Rabs (f x) - Rabs l / 2 + (Rabs l - Rabs (f x))) with (Rabs l / 2). ++ unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; cut (f x <> 0). ** intro; replace (/ f x + - / l) with ((l - f x) * / (l * f x)). { rewrite Rabs_mult; rewrite Rabs_inv. cut (/ Rabs (l * f x) < 2 / Rsqr l). - intro; rewrite Rabs_minus_sym in H5; cut (0 <= / Rabs (l * f x)). + intro; generalize (Rmult_le_0_lt_compat (Rabs (l - f x)) (eps * (Rsqr l / 2)) (/ Rabs (l * f x)) (2 / Rsqr l) (Rabs_pos (l - f x)) H18 H5 H17); replace (eps * (Rsqr l / 2) * (2 / Rsqr l)) with eps. * intro; assumption. * unfold Rdiv; unfold Rsqr; rewrite Rinv_mult. field. exact H0. + left; apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply prod_neq_R0; assumption. - rewrite Rmult_comm; rewrite Rabs_mult; rewrite Rinv_mult. rewrite (Rsqr_abs l); unfold Rsqr; unfold Rdiv; rewrite Rinv_mult. repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r. + apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. + apply Rmult_lt_reg_l with (Rabs (f x) * Rabs l * / 2). * repeat apply Rmult_lt_0_compat. -- apply Rabs_pos_lt; assumption. -- apply Rabs_pos_lt; assumption. -- apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H17; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H17))); unfold INR; intro H18; assumption | discriminate ]. * replace (Rabs (f x) * Rabs l * / 2 * / Rabs (f x)) with (Rabs l / 2). -- replace (Rabs (f x) * Rabs l * / 2 * (2 * / Rabs l)) with (Rabs (f x)). ++ assumption. ++ field. apply Rabs_no_R0. assumption. -- field. apply Rabs_no_R0; assumption. } field. now split. ** red; intro; rewrite H16 in H15; rewrite Rabs_R0 in H15; cut (0 < Rabs l / 2). { intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (Rabs l / 2) 0 H17 H15)). } unfold Rdiv; apply Rmult_lt_0_compat. { apply Rabs_pos_lt; assumption. } apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H17; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H17))); unfold INR; intro; assumption | discriminate ]. ++ pattern (Rabs l) at 3; rewrite <-Rplus_half_diag. ring. -- split; [ assumption | apply Rlt_le_trans with (Rmin delta1 delta2); [ assumption | apply Rmin_r ] ]. * split; [ assumption | apply Rlt_le_trans with (Rmin delta1 delta2); [ assumption | apply Rmin_l ] ]. + change (0 < eps * (Rsqr l / 2)); unfold Rdiv; repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat. * assumption. * apply Rmult_lt_0_compat. -- apply Rsqr_pos_lt; assumption. -- apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H3; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H3))); unfold INR; intro; assumption | discriminate ]. - change (0 < Rabs l / 2); unfold Rdiv; apply Rmult_lt_0_compat; [ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H3; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H3))); unfold INR; intro; assumption | discriminate ] ]. Qed.
imports: Rbase Rfunctions Lra