proposition: Lemma Zle_cast_embedding' : OrderEmbedding (cast N Z).
proof: 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.
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