proposition: Lemma R_plus_assoc : associative R_plus.
proof: Proof. intros x y z Hap. elim Hap; clear Hap; intro H; elim H; intros N HN; elim HN; clear H HN; intros e He HN; simpl in HN; apply (less_irreflexive_unfolded _ e). apply leEq_less_trans with (CS_seq _ x N[+]CS_seq _ y N[+]CS_seq _ z N[-] (CS_seq _ x N[+] (CS_seq _ y N[+]CS_seq _ z N))); auto. rstepl ([0]:F); auto. apply leEq_less_trans with (CS_seq _ x N[+] (CS_seq _ y N[+]CS_seq _ z N) [-] (CS_seq _ x N[+]CS_seq _ y N[+]CS_seq _ z N)); auto. rstepl ([0]:F); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection