proposition: Lemma Z_full_psorder' : FullPseudoOrder Zle Zlt.
proof: Proof. split;[apply _|split;try apply _|]. - apply (Z_ind2 _). intros a b;rewrite !Zlt_def;unfold PairT.Tlt. apply pseudo_order_antisym. - hnf. intros a b E c;revert a b c E. apply (Z_ind3 (fun _ _ _ => _ -> _)). intros [pa na] [pb nb] [pc nc];rewrite !Zlt_def;unfold PairT.Tlt. intros E1. apply (strictly_order_preserving (+ nc)) in E1. eapply (merely_destruct (cotransitive E1 _));intros [E2|E2];apply tr. + left. apply (strictly_order_reflecting ((nb) +)). assert (Hrw : nb + (pa + nc) = pa + nb + nc) by ring_with_nat;rewrite Hrw;exact E2. + right. apply (strictly_order_reflecting ((na) +)). assert (Hrw : na + (pc + nb) = nb + (pc + na)) by ring_with_nat;rewrite Hrw;clear Hrw. assert (Hrw : na + (pb + nc) = pb + na + nc) by ring_with_nat;rewrite Hrw;clear Hrw. trivial. - apply @Z_ind2. + intros a b. apply @istrunc_prod;[|apply _]. apply (@istrunc_arrow _). apply ishprop_sum;try apply _. intros E1 E2;apply (irreflexivity lt a). transitivity b;trivial. + intros a b;rewrite Zapart_def,!Zlt_def;unfold PairT.Tapart,PairT.Tlt. apply apart_iff_total_lt. - apply (Z_ind2 _). intros a b;rewrite Zle_def,Zlt_def;unfold PairT.Tlt,PairT.Tle. apply le_iff_not_lt_flip. Qed.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals