proposition: Lemma R_inv_is_inv : forall x, R_plus x (R_inv x) [=] R_zero.
proof: Proof. intro x; intro x_ap. apply (R_lt_irreflexive R_zero). elim x_ap; clear x_ap; intro x_lt; 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. simpl in |- *; astepr ([0][-] (CS_seq _ x n[+][--] (CS_seq _ x n))); auto. simpl in |- *; astepr (CS_seq _ x n[+][--] (CS_seq _ x n) [-][0]); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection