Fin

\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Arith.Int
\import Arith.Nat
\import Function.Meta
\import HLevel
\import Logic
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin.Pigeonhole

\lemma hasFiniteOrder {G : Group} {P : PigeonholeSet G} (g : G) : ∃ (n : Nat) (n > 0) (G.pow g n = 1)
  => TruncP.map (P.pigeonhole< (\lam n => G.pow g n)) \lam (i,j,i<j,p) =>
      (j -' i, pos<pos.conv $ transportInv (_ <) (-'=- $ <=-less i<j) linarith, cancel_*-right (G.pow g i) $ inv G.pow_+ *> pmap (G.pow g) (unpos $ pmap (`+ pos i) (-'=- $ <=-less i<j) *> linarith) *> inv p *> inv ide-left)

\sfunc order {G : Group} {P : PigeonholeSet G} {D : DecSet G} (g : G) : Nat
  => (aux g).1
  \where {
    \func aux {G : Group} {P : PigeonholeSet G} {D : DecSet G} (g : G)
      : \Sigma (n : Nat) (\Sigma (n > 0) (G.pow g n = 1)) (\Pi (m : Nat) -> (\Sigma (m > 0) (G.pow g m = 1)) -> n <= m)
      => Contr.center {search _ (\lam n => later \have t => LinearOrder.<-dec 0 n \in decide) $ TruncP.map (hasFiniteOrder g) \lam t => (t.1, (t.2, t.3))}
  }

\lemma order>0 {G : Group} {P : PigeonholeSet G} {D : DecSet G} {g : G} : order g > 0
  => rewrite (\peval order g) (order.aux g).2.1

\lemma order_pow {G : Group} {P : PigeonholeSet G} {D : DecSet G} {g : G} : G.pow g (order g) = 1
  => rewrite (\peval order g) (order.aux g).2.2

\lemma order-min {G : Group} {P : PigeonholeSet G} {D : DecSet G} {g : G} {m : Nat} (p : m > 0) (q : G.pow g m = 1) : order g <= m
  => rewrite (\peval order g) $ (order.aux g).3 m (p,q)