proposition: Lemma R_mult_comm : forall x y, R_mult x y [=] R_mult 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