Zle_cast_embedding' : OrderEmbedding (cast N Z). Proof. split;red. - intros. rewrite Zle_def. unfold PairT.Tle. simpl. rewrite 2!plus_0_r;trivial. - intros ??. rewrite Zle_def. unfold PairT.Tle. simpl. rewrite 2!plus_0_r;trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.