proposition: Lemma Zle_plus_preserving_l' : forall z : Z, OrderPreserving ((+) z).
proof: Proof. red. apply (Z_ind3 (fun _ _ _ => _ -> _)). intros [pc nc] [pa na] [pb nb]. rewrite !Zle_def;unfold PairT.Tle;simpl. intros E. assert (Hrw : pc + pa + (nc + nb) = (pc + nc) + (pa + nb)) by ring_with_nat. rewrite Hrw;clear Hrw. assert (Hrw : pc + pb + (nc + na) = (pc + nc) + (pb + na)) by ring_with_nat. rewrite Hrw;clear Hrw. apply (order_preserving _),E. 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