proposition: Lemma ratInverse_continuous : forall c, ~ c == 0 -> continuous_at (fun v' r : Rat => r == ratInverse v') c.
proof: Proof. unfold continuous_at, rat_limit in *. intuition. exists (minRat (c * (1 / 2)) (c * (1/2) * c * epsilon)). intuition. unfold minRat in *. destruct (bleRat (c * (1 / 2)) (c * (1 / 2) * c * epsilon)). apply ratMult_0 in H2; intuition. apply ratMult_0 in H2; intuition. apply ratMult_0 in H3; intuition. apply ratMult_0 in H2; intuition. rewrite H2. rewrite H0. assert (ratDistance x c <= c * (1/2)). eapply leRat_trans. eapply H3. eapply minRat_le_l. assert (ratSubtract c (c * (1/2)) <= x). eapply ratDistance_ge_difference. rewrite ratDistance_comm. trivial. assert (x <= c + (c * (1/2))). eapply ratDistance_le_sum. trivial. assert (c * (1/2) <= x). rewrite <- (ratSubtract_half). trivial. clear H5. assert (x <= c * (3/2)). rewrite ratMult_ratAdd_cd in H6. simpl in *. trivial. clear H6. assert (ratInverse x <= ratInverse (c * (1 / 2))). apply ratInverse_leRat. intuition. apply ratMult_0 in H6; intuition. trivial. rewrite ratDistance_ratInverse. rewrite H3. rewrite minRat_le_r. rewrite ratInverse_ratMult; intuition. rewrite H6. rewrite ratInverse_ratMult; intuition. rewrite ratMult_comm. repeat rewrite <- ratMult_assoc. rewrite (ratMult_assoc ((ratInverse c) * (ratInverse (1/2)))). rewrite ratInverse_prod_1; intuition. rewrite ratMult_1_r. rewrite (ratMult_assoc (ratInverse c)). rewrite ratInverse_prod_1; intuition. rewrite ratMult_1_r. rewrite ratInverse_prod_1; intuition. rewrite ratMult_1_l. intuition. rewrite H8 in H7. assert (c * (1 / 2) == 0). eapply leRat_impl_eqRat. trivial. eapply rat0_le_all. apply ratMult_0 in H9; intuition. intuition. rewrite H8 in H7. assert (c * (1 / 2) == 0). eapply leRat_impl_eqRat. trivial. eapply rat0_le_all. apply ratMult_0 in H9; intuition. intuition. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith