proposition: Lemma R_inv_ext : un_op_strext _ R_inv.
proof: Proof. intros x y Hxy. elim Hxy; clear Hxy; intro x_lt; [ right | left ]; elim x_lt; intros N H; elim H; clear x_lt H; intros e He HN; exists N; exists e; auto; simpl in HN; intros n Hn. rstepr ([--] (CS_seq _ y n) [-][--] (CS_seq _ x n)); auto. rstepr ([--] (CS_seq _ x n) [-][--] (CS_seq _ y n)); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection