proposition: Lemma negligible_plus : forall f1 f2, negligible f1 -> negligible f2 -> negligible (fun n => f1 n + f2 n)%rat.
proof: Proof. unfold negligible in *. intuition. destruct (H (S c)). destruct (H0 (S c)). exists (max 1 (max x x0)). intuition. apply Nat.max_lub_lt_iff in H3. intuition. assert (1 / expnat x1 c <= 2/1 * (maxRat (f1 x1) (f2 x1)))%rat. eapply leRat_trans. eapply H4. eapply ratAdd_2_ratMax. assert (1 / expnat x1 (S c) <= RatIntro 1 (posnatMult (pos 2) (pos (expnat x1 c))))%rat. eapply leRat_terms; intuition. unfold natToPosnat, posnatToNat, posnatMult. eapply expnat_double_le. lia. unfold maxRat in *. case_eq (bleRat (f1 x1) (f2 x1)); intuition. rewrite H8 in H3. eapply H2. eapply Nat.le_lt_trans. eapply Nat.le_max_r. eauto. rewrite H7. rewrite rat_mult_den. rewrite H3. rewrite <- ratMult_assoc. rewrite <- ratMult_num_den. rewrite num_dem_same_rat1. rewrite ratMult_1_l. intuition. unfold posnatMult, natToPosnat, posnatToNat. lia. rewrite H8 in H3. eapply H1. eapply Nat.le_lt_trans. eapply Nat.le_max_l. eauto. rewrite H7. rewrite rat_mult_den. rewrite H3. rewrite <- ratMult_assoc. rewrite <- ratMult_num_den. rewrite num_dem_same_rat1. rewrite ratMult_1_l. intuition. unfold posnatMult, natToPosnat, posnatToNat. lia. Qed.
imports: FCF.StdNat FCF.Rat