proposition: Lemma rat_inf_limit_difference : 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 => (ratSubtract_rel (f1 n) (f2 n))) (ratSubtract c1 c2).
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. destruct (le_Rat_dec c1 c2). edestruct (H1 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. edestruct (H2 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. exists (Nat.max x x0). intuition. unfold ratSubtract_rel in *. destruct (H n'). destruct (H0 n'). rewrite H7; eauto. rewrite (ratSubtract_0 l). eapply ratDistance_0_r_le. eapply leRat_trans. eapply ratSubtract_partition_leRat. eapply ratSubtract_ratDistance_le. 2:{ rewrite H4. rewrite ratHalf_add. intuition. eapply Nat.max_lub_l. eauto. trivial. } eapply leRat_trans. eapply ratSubtract_partition_leRat. rewrite ratSubtract_0. eapply leRat_refl. eapply l. eapply ratSubtract_ratDistance_le. rewrite ratDistance_comm. rewrite H5. rewrite <- ratAdd_0_l. intuition. eapply Nat.max_lub_r. eauto. trivial. edestruct (H1 (minRat (ratHalf epsilon) (ratHalf (ratSubtract c1 c2)))). intuition. unfold minRat in *. destruct (bleRat (ratHalf epsilon) (ratHalf (ratSubtract c1 c2))). eapply ratHalf_ne_0 in H4; intuition. eapply ratHalf_ne_0 in H4; intuition. eapply n. eapply ratSubtract_0_inv. trivial. edestruct (H2 (minRat (ratHalf epsilon) (ratHalf (ratSubtract c1 c2)))). intuition. unfold minRat in *. destruct (bleRat (ratHalf epsilon) (ratHalf (ratSubtract c1 c2))). eapply ratHalf_ne_0 in H5; intuition. eapply ratHalf_ne_0 in H5; intuition. eapply n. eapply ratSubtract_0_inv. trivial. exists (Nat.max x x0). intuition. destruct (H n'). destruct (H0 n'). unfold ratSubtract_rel in *. rewrite H7; eauto. assert (x2 <= x1). eapply leRat_trans. eapply ratDistance_le_sum. eapply H5. eapply Nat.max_lub_r. eauto. trivial. eapply leRat_trans. eapply ratAdd_leRat_compat. eapply leRat_refl. eapply minRat_le_r. eapply (leRat_ratAdd_same_r (ratHalf (ratSubtract c1 c2))). rewrite ratAdd_assoc. rewrite ratHalf_add. rewrite ratSubtract_ratAdd_inverse_2. eapply ratDistance_le_sum. eapply leRat_trans. rewrite ratDistance_comm. eapply H4. eapply Nat.max_lub_l. eauto. trivial. eapply minRat_le_r. case_eq (bleRat c1 c2); intuition. eapply bleRat_total. trivial. eapply leRat_trans. eapply rat_distance_of_difference. trivial. case_eq (bleRat c1 c2); intuition. eapply bleRat_total. trivial. eapply H4. eapply Nat.max_lub_l. eauto. trivial. eapply H5. eapply Nat.max_lub_r. eauto. trivial. rewrite minRat_le_l. rewrite ratHalf_add. intuition. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith