diff --git a/theories/Algebra/Groups.v b/theories/Algebra/Groups.v
index 8ba845aabe..89d347bd34 100644
--- a/theories/Algebra/Groups.v
+++ b/theories/Algebra/Groups.v
@@ -13,7 +13,7 @@ Require Export HoTT.Algebra.Groups.FreeProduct.
 
 Require Export HoTT.Algebra.Groups.Presentation.
 Require Export HoTT.Algebra.Groups.ShortExactSequence.
-Require Export HoTT.Algebra.Groups.Lagrange.
+Require Export HoTT.Algebra.Groups.Finite.
 
 (** Examples *)
 
diff --git a/theories/Algebra/Groups/Finite.v b/theories/Algebra/Groups/Finite.v
new file mode 100644
index 0000000000..8a9cceb2ca
--- /dev/null
+++ b/theories/Algebra/Groups/Finite.v
@@ -0,0 +1,64 @@
+Require Import Basics Types.
+Require Import Algebra.Groups.Group.
+Require Import Algebra.Groups.Subgroup.
+Require Import Algebra.Groups.QuotientGroup.
+Require Import Spaces.Finite.Finite.
+Require Import Spaces.Nat.Core Spaces.Nat.Division.
+Require Import Truncations.Core.
+
+Local Open Scope nat_scope.
+Local Open Scope mc_mult_scope.
+
+Set Universe Minimization ToSet.
+
+(** * Finite Groups *)
+
+(** ** Basic Properties *)
+
+(** The order of a group is strictly positive. *)
+Global Instance lt_zero_fcard_grp (G : Group) (fin_G : Finite G) : 0 < fcard G.
+Proof.
+  pose proof (merely_equiv_fin G) as f.
+  strip_truncations.
+  destruct (fcard G).
+  - contradiction (f mon_unit).
+  - exact _.
+Defined.
+
+(** ** Lagrange's theorem *)
+
+(** Lagrange's Theorem - Given a finite group [G] and a finite subgroup [H] of [G], the order of [H] divides the order of [G].
+
+Note that constructively, a subgroup of a finite group cannot be shown to be finite without excluded middle. We therefore have to assume it is. This in turn implies that the subgroup is decidable. *)
+Definition divides_fcard_subgroup {U : Univalence}
+  (G : Group) (H : Subgroup G) {fin_G : Finite G} {fin_H : Finite H}
+  : (fcard H | fcard G).
+Proof.
+  exists (subgroup_index G H).
+  symmetry.
+  refine (fcard_quotient (in_cosetL H) @ _).
+  refine (_ @ finadd_const _ _).
+  apply ap, path_forall.
+  srapply Quotient_ind_hprop; simpl.
+  intros x.
+  apply fcard_equiv'.
+  apply equiv_sigma_in_cosetL_subgroup.
+Defined.
+
+(** As a corollary, the index of a subgroup is the order of the group divided by the order of the subgroup. *)
+Definition subgroup_index_fcard_div {U : Univalence}
+  (G : Group) (H : Subgroup G) (fin_G : Finite G) (fin_H : Finite H)
+  : subgroup_index G H = fcard G / fcard H.
+Proof.
+  rapply nat_div_moveL_nV.
+  apply divides_fcard_subgroup.
+Defined.
+
+(** Therefore we can show that the order of the quotient group [G / H] is the order of [G] divided by the order of [H]. *)
+Definition fcard_grp_quotient {U : Univalence}
+  (G : Group) (H : NormalSubgroup G)
+  (fin_G : Finite G) (fin_H : Finite H)
+  : fcard (QuotientGroup G H) = fcard G / fcard H.
+Proof.
+  rapply subgroup_index_fcard_div.
+Defined.
diff --git a/theories/Algebra/Groups/Lagrange.v b/theories/Algebra/Groups/Lagrange.v
deleted file mode 100644
index 749d78771d..0000000000
--- a/theories/Algebra/Groups/Lagrange.v
+++ /dev/null
@@ -1,53 +0,0 @@
-Require Import Basics Types.
-Require Import Algebra.Groups.Group.
-Require Import Algebra.Groups.Subgroup.
-Require Import Algebra.Groups.QuotientGroup.
-Require Import Spaces.Finite.Finite.
-Require Import Spaces.Nat.Core.
-
-(** ** Lagrange's theorem *)
-
-Local Open Scope mc_scope.
-Local Open Scope mc_mult_scope.
-Local Open Scope nat_scope.
-
-Definition subgroup_index {U : Univalence} (G : Group) (H : Subgroup G)
-  (fin_G : Finite G) (fin_H : Finite H)
-  : nat.
-Proof.
-  refine (fcard (Quotient (in_cosetL H))).
-  nrapply finite_quotient.
-  1-5: exact _.
-  intros x y.
-  pose (dec_H := detachable_finite_subset H).
-  apply dec_H.
-Defined.
-
-(** Given a finite group G and a finite subgroup H of G, the order of H divides the order of G. Note that constructively, a subgroup of a finite group cannot be shown to be finite without exlcluded middle. We therefore have to assume it is. This in turn implies that the subgroup is decidable. *)
-Theorem lagrange {U : Univalence} (G : Group) (H : Subgroup G)
-  (fin_G : Finite G) (fin_H : Finite H)
-  : exists d, d * (fcard H) = fcard G.
-Proof.
-  exists (subgroup_index G H _ _).
-  symmetry.
-  refine (fcard_quotient (in_cosetL H) @ _).
-  refine (_ @ finadd_const _ _).
-  apply ap, path_forall.
-  srapply Quotient_ind_hprop.
-  simpl. (** simpl is better than cbn here *)
-  intros x.
-  apply fcard_equiv'.
-  (** Now we must show that cosets are all equivalent as types. *)
-  simpl.
-  snrapply equiv_functor_sigma.
-  2: apply (isequiv_group_left_op x^).
-  1: hnf; trivial.
-  exact _.
-Defined.
-
-Corollary lagrange_normal {U : Univalence} (G : Group) (H : NormalSubgroup G)
-  (fin_G : Finite G) (fin_H : Finite H)
-  : fcard (QuotientGroup G H) * fcard H = fcard G.
-Proof.
-  apply lagrange.
-Defined.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index 4aebf2f80b..c19b207626 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -17,6 +17,8 @@ Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.
 Local Open Scope wc_iso_scope.
 
+(** ** Congruence quotients *)
+
 Section GroupCongruenceQuotient.
 
   (** A congruence on a group is a relation satisfying [R x x' -> R y y' -> R (x * y) (x' * y')].  Because we also require that [R] is reflexive, we also know that [R y y' -> R (x * y) (x * y')] for any [x], and similarly for multiplication on the right by [x].  We don't need to assume that [R] is symmetric or transitive. *)
@@ -106,6 +108,55 @@ Section GroupCongruenceQuotient.
 
 End GroupCongruenceQuotient.
 
+(** ** Sets of cosets *)
+
+Section Cosets.
+
+  Context (G : Group) (H : Subgroup G).
+  
+  Definition LeftCoset := G / in_cosetL H.
+
+  (** TODO: Way too many universes, needs fixing *)
+  (** The set of left cosets of a finite subgroup of a finite group is finite. *)
+  Global Instance finite_leftcoset `{Univalence, Finite G, Finite H}
+    : Finite LeftCoset.
+  Proof.
+    nrapply finite_quotient.
+    1-5: exact _.
+    intros x y.
+    apply (detachable_finite_subset H).
+  Defined.
+
+  (** The index of a subgroup is the number of cosets of the subgroup. *)
+  Definition subgroup_index `{Univalence, Finite G, Finite H} : nat
+    := fcard LeftCoset.
+
+  Definition RightCoset := G / in_cosetR H.
+  
+  (** The set of left cosets is equivalent to the set of right coset. *)
+  Definition equiv_leftcoset_rightcoset
+    : LeftCoset <~> RightCoset.
+  Proof.
+    snrapply equiv_quotient_functor.
+    - exact inv.
+    - exact _.
+    - intros x y; simpl.
+      by rewrite grp_inv_inv.
+  Defined.
+
+  (** The set of right cosets of a finite subgroup of a finite group is finite since it is equivalent to the set of left cosets. *)
+  Global Instance finite_rightcoset `{Univalence, Finite G, Finite H}
+    : Finite RightCoset.
+  Proof.
+    nrapply finite_equiv'.
+    1: apply equiv_leftcoset_rightcoset.
+    exact _.
+  Defined.
+
+End Cosets.
+
+(** ** Quotient groups *)
+
 (** Now we can define the quotient group by a normal subgroup. *)
 
 Section QuotientGroup.
@@ -126,7 +177,7 @@ Section QuotientGroup.
 
   (** Now we have to make a choice whether to pick the left or right cosets. Due to existing convention we shall pick left cosets but we note that we could equally have picked right. *)
   Definition QuotientGroup : Group
-    := Build_Group (G / (in_cosetL N)) _ _ _ _.
+    := Build_Group (LeftCoset G N) _ _ _ _.
 
   Definition grp_quotient_map : G $-> QuotientGroup.
   Proof.
@@ -343,7 +394,7 @@ Proof.
   simpl in triv.
   apply related_quotient_paths in triv.
   2-5: exact _.
-  apply equiv_subgroup_inverse.
+  apply equiv_subgroup_inv.
   nrapply (subgroup_in_op_l _ _ 1 triv) .
   apply subgroup_in_unit.
 Defined.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index b5356e5bef..78a49bc07a 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -139,9 +139,16 @@ Proof.
   apply subgroup_in_inv'.
 Defined.
 
-Definition equiv_subgroup_inverse {G : Group} (H : Subgroup G) (x : G)
+Definition equiv_subgroup_inv {G : Group} (H : Subgroup G) (x : G)
   : H x <~> H x^ := Build_Equiv _ _ (subgroup_in_inv H x) _.
 
+Definition equiv_subgroup_op_inv {G : Group} (H : Subgroup G) (x y : G)
+  : H (x * y^) <~> H (y * x^).
+Proof.
+  nrefine (_ oE equiv_subgroup_inv _ _).
+  by rewrite grp_inv_op, grp_inv_inv.
+Defined.
+
 (** The group given by a subgroup *)
 Definition subgroup_group {G : Group} (H : Subgroup G) : Group.
 Proof.
@@ -366,6 +373,25 @@ Proof.
   all: by intro.
 Defined.
 
+(** The sigma type of a left coset is equivalent to the sigma type of the subgroup. *)
+Definition equiv_sigma_in_cosetL_subgroup (G : Group) (H : Subgroup G) (x : G)
+  : sig (in_cosetL H x) <~> sig H.
+Proof.
+  snrapply equiv_functor_sigma'.
+  - rapply (Build_Equiv _ _ (x^ *.)).
+  - reflexivity.
+Defined.
+
+(** The sigma type of a right coset is equivalent to the sigma type of the subgroup. *)
+Definition equiv_sigma_in_cosetR_subgroup (G : Group) (H : Subgroup G) (x : G)
+  : sig (in_cosetR H x) <~> sig H.
+Proof.
+  snrapply equiv_functor_sigma'.
+  - rapply (Build_Equiv _ _ (.* x ^)).
+  - simpl; intros y.
+    apply equiv_subgroup_op_inv.
+Defined.
+
 (** A normal subgroup is a subgroup closed under conjugation. *)
 Class IsNormalSubgroup {G : Group} (N : Subgroup G)
   := isnormal : forall {x y}, N (x * y) -> N (y * x).
diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v
index 9f55599467..d52a82f016 100644
--- a/theories/Spaces/Nat/Division.v
+++ b/theories/Spaces/Nat/Division.v
@@ -631,6 +631,15 @@ Proof.
   nrapply nat_mod_mul_l.
 Defined.
 
+(** We can move a divisor from the right to become a factor on the left of an equation. *)
+Definition nat_div_moveL_nV n m k : 0 < k -> n * k = m -> n = m / k.
+Proof.
+  intros H p.
+  rewrite <- p.
+  symmetry.
+  rapply nat_div_mul_cancel_r.
+Defined.
+
 (** ** Greatest Common Divisor *)
 
 (** The greatest common divisor of [0] and a number is the number itself. *)