proposition: Lemma R_ap_alt_1 : forall x y : R_CSetoid, x [#] y -> {e : F | [0] [<] e | {N : nat | forall m, N <= m -> AbsBig e (CS_seq F x m[-]CS_seq F y m)}}.
proof: Proof. intros x y H. case H; intros H0. case H0; intros N1 HN1. case HN1; intros e1 H2 H31. exists e1. assumption. exists N1. split. assumption. right. apply inv_cancel_leEq. rstepl e1. rstepr (CS_seq F y m[-]CS_seq F x m). apply H31. assumption. case H0; intros N1 HN1. case HN1; intros e1 H2 H31. exists e1. assumption. exists N1. split; try left; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection