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