proposition: Lemma Z_partial_order' : PartialOrder Zle.
proof: Proof. split;[apply _|apply _|split|]. - hnf. apply (Z_ind _). intros. change (PairT.Tle x x). red. reflexivity. - hnf. apply (Z_ind3 (fun _ _ _ => _ -> _ -> _)). intros [pa na] [pb nb] [pc nc]. rewrite !Zle_def;unfold PairT.Tle;simpl. intros E1 E2. apply (order_reflecting (+ (nb + pb))). assert (Hrw : pa + nc + (nb + pb) = (pa + nb) + (pb + nc)) by abstract ring_with_nat. rewrite Hrw;clear Hrw. assert (Hrw : pc + na + (nb + pb) = (pb + na) + (pc + nb)) by abstract ring_with_nat. rewrite Hrw;clear Hrw. apply plus_le_compat;trivial. - hnf. apply (Z_ind2 (fun _ _ => _ -> _ -> _)). intros [pa na] [pb nb];rewrite !Zle_def;unfold PairT.Tle;simpl. intros E1 E2;apply Z_path;red;simpl. apply (antisymmetry le);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