proposition: Lemma rat_inf_limit_product : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, left_total f1 -> left_total f2 -> rat_inf_limit f1 c1 -> rat_inf_limit f2 c2 -> rat_inf_limit (fun n => (ratMult_rel (f1 n) (f2 n))) (c1 * c2).
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. edestruct (H1 ((ratInverse (1 + c2)) * epsilon * (1/ 2))). intuition. apply ratMult_0 in H4. intuition. apply ratMult_0 in H5. intuition. eapply ratInverse_nz. eauto. edestruct (H2 ((ratInverse (1 + c1)) * epsilon * (1 / 2))). intuition. apply ratMult_0 in H5. intuition. apply ratMult_0 in H6. intuition. eapply ratInverse_nz. eauto. edestruct (H2 1). intuition. exists (maxList (x :: x0 :: x1 :: nil)). intuition. unfold ratMult_rel in *. edestruct H. edestruct H0. rewrite H8; eauto. eapply leRat_trans. eapply (ratTriangleInequality _ _ (c1 * x3)). rewrite ratMult_ratDistance_factor_r. rewrite ratMult_ratDistance_factor_l. rewrite ratMult_comm. eapply leRat_trans. eapply ratAdd_leRat_compat. eapply ratMult_leRat_compat. eapply ratDistance_le_sum. eapply H6; [idtac | eapply H10]. eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. trivial. eapply H4; [idtac | eapply H9]. eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. trivial. eapply ratMult_leRat_compat. eapply (ratAdd_any_leRat_l 1). eapply leRat_refl. eapply H5; [idtac | eapply H10]. eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. trivial. eapply eqRat_impl_leRat. repeat rewrite <- ratMult_assoc. rewrite (ratAdd_comm c2). rewrite (ratAdd_comm c1). rewrite (ratMult_assoc ((1 + c2) * (ratInverse (1 + c2)))). rewrite (ratMult_assoc ((1 + c1) * (ratInverse (1 + c1)))). rewrite <- ratMult_distrib_r. rewrite (ratMult_comm (1 + c2)). rewrite (ratMult_comm (1 + c1)). repeat rewrite ratInverse_prod_1. rewrite ratMult_2. rewrite ratMult_1_l. rewrite ratMult_comm. rewrite ratMult_assoc. rewrite ratMult_eq_rat1. eapply ratMult_1_r. intuition. assert (1 <= 0). eapply leRat_trans. eapply (ratAdd_any_leRat_r c1). eapply leRat_refl. eapply eqRat_impl_leRat. rewrite ratAdd_comm. trivial. intuition. intuition. assert (1 <= 0). eapply leRat_trans. eapply (ratAdd_any_leRat_r c2). eapply leRat_refl. eapply eqRat_impl_leRat. rewrite ratAdd_comm. trivial. intuition. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith