PseudoSemiRingOrder (<). Proof. split; try apply _. - intros x y E. apply srorder_partial_minus, not_lt_le_flip;trivial. - intros z. repeat (split; try apply _). intros x y E. apply lt_correct in E;apply lt_correct. destruct E as [E2a E2b]. split. + apply (order_preserving (z+));trivial. + intros E3. apply E2b. apply (left_cancellation (+) z);trivial. - apply (apartness.dec_strong_binary_morphism (.*.)). - intros x y E1 E2. apply lt_correct in E1;apply lt_correct in E2;apply lt_correct. destruct E1 as [E1a E1b], E2 as [E2a E2b]. split. + apply nonneg_mult_compat;trivial. + apply symmetric_neq. apply mult_ne_0; apply symmetric_neq;trivial. Qed.
Require Import