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