nat_full' : FullPseudoSemiRingOrder nat_le nat_lt. Proof. split;[apply _|split|]. - split;try apply _. + intros a b [E1 E2]. destruct (irreflexivity lt a). transitivity b;trivial. + hnf. intros a b E c;apply tr;apply lt_strong_cotrans;trivial. + reflexivity. - intros a b E. apply nat_not_lt_le,le_exists in E. destruct E as [k E];exists k;rewrite plus_comm;auto. - split. + intros a b E. apply le_exists in E;destruct E as [k Hk]. rewrite Hk. rewrite add_S_r,<-add_S_l. rewrite plus_assoc,(plus_comm z (S k)), <-plus_assoc. apply le_S_S,le_plus. + intros a b E. apply le_exists in E;destruct E as [k E]. rewrite <-add_S_r,plus_assoc,(plus_comm k z),<-plus_assoc in E. apply (left_cancellation plus _) in E. rewrite E;apply le_plus. - intros ???? E. apply trivial_apart in E. destruct (dec (apart x₁ x₂)) as [?|ex];apply tr;auto. right. apply tight_apart in ex. apply trivial_apart. intros ey. apply E. apply ap011;trivial. - unfold PropHolds. intros a b Ea Eb. apply nonzero_gt_0. intros E. apply mult_eq_zero in E. destruct E as [E|E];[rewrite E in Ea|rewrite E in Eb]; apply (irreflexivity lt 0);trivial. - intros a b;split. + intros E1 E2. apply nat_lt_not_le in E2. auto. + intros E. destruct (le_lt_dec a b);auto. destruct E;auto. Qed.
Require Import