proposition: Lemma lt_respects@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> Tlt q1 r1 <~> Tlt q2 r2.
proof: Proof. intros. apply equiv_iff_hprop_uncurried. split;apply lt_respects_aux; trivial;apply symmetry;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