proposition: Lemma le_respects_aux@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> Tle q1 r1 -> Tle q2 r2.
proof: Proof. unfold equiv,Tle;intros [pa na] [pb nb] Eq [pc nc] [pd nd] Er E;simpl in *. apply (order_reflecting (+ (pc + na))). assert (Erw : pb + nd + (pc + na) = (pb + na) + (pc + nd)) by ring_with_nat. rewrite Erw,<-Eq,Er;clear Erw. assert (Erw : pa + nb + (pd + nc) = pd + nb + (pa + nc)) by ring_with_nat. rewrite Erw. 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