Zlt_strict' : StrictOrder Zlt. Proof. split. - apply _. - change (forall x, x < x -> Empty). apply (Z_ind (fun _ => _ -> _)). intros [pa na];rewrite Zlt_def;unfold PairT.Tlt;simpl. apply irreflexivity,_. - hnf. apply (Z_ind3 (fun _ _ _ => _ -> _ -> _)). intros [pa na] [pb nb] [pc nc];rewrite !Zlt_def;unfold PairT.Tlt;simpl. intros E1 E2. apply (strictly_order_reflecting (+ (nb + pb))). assert (Hrw : pa + nc + (nb + pb) = (pa + nb) + (pb + nc)) by ring_with_nat. rewrite Hrw;clear Hrw. assert (Hrw : pc + na + (nb + pb) = (pb + na) + (pc + nb)) by ring_with_nat. rewrite Hrw;clear Hrw. apply plus_lt_compat;trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.