proposition: Lemma R_plus_comm : forall x y, R_plus x y [=] R_plus y x.
proof: Proof. intros x y Hxy. elim Hxy; clear Hxy; 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 _ y N[+]CS_seq _ x N[-] (CS_seq _ x N[+]CS_seq _ y N)); auto. rstepl ([0]:F); auto. apply leEq_less_trans with (CS_seq _ x N[+]CS_seq _ y N[-] (CS_seq _ y N[+]CS_seq _ x N)); auto. rstepl ([0]:F); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection