Lagrange

\import Algebra.Group
\import Algebra.Group.SubGroup
\import Algebra.Monoid
\import Arith.Nat
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.Fin
\import Set.Fin.BoundedPigeonhole
\import Set.Fin.Instances
\import Set.Fin.KFin
\import Set.Fin.Pigeonhole
\open Group
\open Monoid(LDiv)

\func lagrange-gen (H : SubGroup) (c : IsSplitSurj H.inc~) : TruncP (QEquiv {H.S} {\Sigma H.Cosets (IGroup H)}) \elim c
  | inP e => inP \new QEquiv {
    | f x => (in~ x, (inverse x * e.1 (in~ x), Quotient.equalityEquiv SubGroup.equivalence $ inv $ e.2 $ in~ x))
    | ret s => e.1 s.1 * inverse s.2.1
    | ret_f x => rewrite (inverse_*, inverse-isInv, inv *-assoc, inverse-right) ide-left
    | f_sec s =>
      \have p : in~ (e.1 s.1 * inverse s.2.1) = s.1 => ~-pequiv (later $ rewrite (inverse_*, inverse-isInv, *-assoc, inverse-left, ide-right) s.2.2) *> e.2 s.1
      \in unfold_let $ pmap2 (__,__) p $ ext $ rewrite (p, inverse_*, inverse-isInv, *-assoc, inverse-left) ide-right
  }

\func lagrange (H : FinSubGroup) : LDiv (IFinGroup H).card (card {H.S}) \cowith
  | inv => (Cosets-fin H H.S).card
  | inv-right => \case lagrange-gen H $ (Cosets-fin H H.S).splitSurj Quotient.in-surj \with {
    | inP p => inv $ card_Equiv {H.S} {ProdFin (Cosets-fin H H.S) (IFinGroup H)} p *> *-comm
  }
  \where {
    \lemma Cosets-fin (H : DecSubGroup) (_ : KFinSet H.S) : FinSet H.Cosets
      => KFinSet.KFin+Dec=>Fin QuotientKFin {QuotientDec \lam g g' => later $ H.isDec _}
  }