proposition: Lemma converges_equiv s t : s == t -> (converges s <-> converges t).
proof: Proof. intros H; split; intros [u [A lu]]; exists u;split;try assumption; rewrite <- A. - symmetry. eassumption. - eassumption. Qed.
imports: Lia