proposition: Lemma R_plus_lft_ext : forall x y z, R_plus x z [#] R_plus y z -> x [#] y.
proof: Proof. intros x y z Hxy. elim Hxy; clear Hxy; intro H; [ left | right ]; elim H; intros N HN; elim HN; clear H HN; intros e He HN; exists N; exists e; auto; intros n Hn; simpl in HN. rstepr (CS_seq _ y n[+]CS_seq _ z n[-] (CS_seq _ x n[+]CS_seq _ z n)); auto. rstepr (CS_seq _ x n[+]CS_seq _ z n[-] (CS_seq _ y n[+]CS_seq _ z n)); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection