Lemma isOneSided_translation : ∏ (D : hq → hProp) (c : hq), isOneSided D → isOneSided (λ q, D (q + c)). Proof. intros D c Hd. split ; split. - generalize (pr1 (pr1 Hd)). apply hinhfun. intros r. exists (pr1 r - c). unfold hqminus. rewrite hqplusassoc, hqlminus, hqplusr0. exact (pr2 r). - generalize (pr2 (pr1 Hd)). apply hinhfun. intros r. exists (pr1 r - c). unfold hqminus. rewrite hqplusassoc, hqlminus, hqplusr0. exact (pr2 r). - intros r D'r. generalize (pr1 (pr2 Hd) _ D'r). apply hinhfun. intros q. exists (pr1 q - c). split. + unfold hqminus. rewrite hqplusassoc, hqlminus, hqplusr0. exact (pr1 (pr2 q)). + apply hqlthandplusrinv with c. unfold hqminus. rewrite hqplusassoc, hqlminus, hqplusr0. exact (pr2 (pr2 q)). - intros r s Hrs. apply (pr2 (pr2 Hd)). apply hqlthandplusr, Hrs. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.