module Data.Int.Order where
Ordering integersπ
private le-lemma : β a b x y β Path (n-Type lzero 1) (el (a + y Nat.β€ b + x) Nat.β€-is-prop) (el (a + suc y Nat.β€ b + suc x) Nat.β€-is-prop) le-lemma a b x y = n-ua (prop-ext Nat.β€-is-prop Nat.β€-is-prop (Ξ» p β transport (apβ Nat._β€_ (sym (Nat.+-sucr a y)) (sym (Nat.+-sucr b x))) (Nat.sβ€s p)) (Ξ» p β Nat.β€-peel (transport (apβ Nat._β€_ (Nat.+-sucr a y) (Nat.+-sucr b x)) p))) le-lemmaβ² : β a b x y β Path (n-Type lzero 1) (el (a + x Nat.β€ b + y) Nat.β€-is-prop) (el (suc (a + x) Nat.β€ suc (b + y)) Nat.β€-is-prop) le-lemmaβ² a b x y = n-ua (prop-ext Nat.β€-is-prop Nat.β€-is-prop Nat.sβ€s Ξ» { (Nat.sβ€s x) β x }) Int-le-prop : Int β Int β Prop lzero Int-le-prop (diff a b) (diff c d) = el (a + d Nat.β€ b + c) Nat.β€-is-prop Int-le-prop (diff a b) (quot x y i) = le-lemma a b x y i Int-le-prop (quot m n i) (diff x y) = le-lemmaβ² m n y x i Int-le-prop (quot a b i) (quot c d j) = is-setβsquarep (Ξ» _ _ β n-Type-is-hlevel 1) (Ξ» i β le-lemmaβ² a b d c i) (Ξ» i β le-lemma a b c d i) (n-ua (prop-ext Nat.β€-is-prop Nat.β€-is-prop (Ξ» p β transport (apβ Nat._β€_ (sym (ap suc (Nat.+-sucr a d))) (sym (ap suc (Nat.+-sucr b c)))) (Nat.sβ€s p)) (Ξ» p β Nat.β€-peel (transport (apβ Nat._β€_ (ap suc (Nat.+-sucr a d)) (ap suc (Nat.+-sucr b c))) p)))) (Ξ» i β le-lemmaβ² a b (suc d) (suc c) i) i j _β€_ : Int β Int β Type x β€ y = β£ Int-le-prop x y β£ β€-refl : β {x} β x β€ x β€-refl {x} = Int-elim-prop {P = Ξ» x β x β€ x} (Ξ» _ β hlevel!) (Ξ» a b β subst (a + b Nat.β€_) (Nat.+-commutative a b) Nat.β€-refl) x private sumβ€0-l : β x y β (x + y) Nat.β€ 0 β x β‘ 0 sumβ€0-l zero zero p = refl sumβ€0-r : β x y β (x + y) Nat.β€ 0 β y β‘ 0 sumβ€0-r zero zero p = refl β€-trans : β {x y z} β x β€ y β y β€ z β x β€ z β€-trans {x} {y} {z} p q with by-sign x | by-sign y | by-sign z ... | negv x | posv y | posv z = Nat.0β€x ... | negv x | negv y | posv z = Nat.0β€x ... | posv x | posv y | posv z = Nat.β€-trans p (subst (Nat._β€ z) (Nat.+-zeror y) q) ... | negv x | negv y | negv z = Nat.β€-trans q (subst (Ξ» e β suc e Nat.β€ suc (x + 0)) (sym (Nat.+-zeror y)) p) ... | posv x | posv y | negv z = absurd (Nat.zeroβ suc (sym (sumβ€0-r y (suc z) q))) ... | posv x | negv y | posv z = absurd (Nat.zeroβ suc (sym (sumβ€0-r x (suc y) p))) ... | posv x | negv y | negv z = absurd (Nat.zeroβ suc (sym (sumβ€0-r x (suc y) p))) ... | negv x | posv y | negv z = absurd (Nat.zeroβ suc (sym (sumβ€0-r y (suc z) q))) β€-antisym : β {x y} β x β€ y β y β€ x β x β‘ y β€-antisym {x} {y} p q with by-sign x | by-sign y ... | posv x | negv y = absurd (Nat.zeroβ suc (sym (sumβ€0-r x (suc y) p))) ... | negv x | posv y = absurd (Nat.zeroβ suc (sym (sumβ€0-r y (suc x) q))) ... | negv x | negv y = ap (Ξ» e β diff 0 (suc e)) $ Nat.β€-antisym (subst (x Nat.β€_) (Nat.+-zeror y) (Nat.β€-peel q)) (subst (y Nat.β€_) (Nat.+-zeror x) (Nat.β€-peel p)) ... | posv x | posv y = ap (Ξ» e β diff e 0) $ Nat.β€-antisym (subst (Nat._β€ y) (Nat.+-zeror x) p) (subst (Nat._β€ x) (Nat.+-zeror y) q)