proposition: Theorem limits_eq : forall f a1 a2, left_total f -> inf_limit f a1 -> inf_limit f a2 -> eq a1 a2.
proof: Proof. intuition. eapply distance_eq_zero. eapply le_epsilon_zero. intuition. eapply limit_eq_h; eauto. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat