theorem Hex.PermGroup.Group.IsSubgroup.order_le {n : Nat} {G H : Group n} (h : H.IsSubgroup G) : H.order ≤ G.order

Subgroup containment bounds exact order, without enumerating either group in the executable operation.

theorem Hex.PermGroup.Group.index_one {n : Nat} {G H : Group n} (h : H.IsSubgroup G) : G.index H h = 1 ↔ SameGroup H G

Index one means equality of the represented groups, independently of generator presentation. The transversal exists only in this erased proof.

theorem Hex.PermGroup.Group.IsSubgroup.order_double {n : Nat} {G H : Group n} (h : H.IsSubgroup G) (hne : ¬SameGroup H G) : 2 * H.order ≤ G.order

A strict subgroup has index at least two, so every strict increase or decrease changes order by a factor of at least two.

theorem Hex.PermGroup.Group.IsSubgroup.order_lt {n : Nat} {G H : Group n} (h : H.IsSubgroup G) (hne : ¬SameGroup H G) : H.order < G.order

theorem Hex.PermGroup.Group.IsSubgroup.order_eq_iff {n : Nat} {G H : Group n} (h : H.IsSubgroup G) : H.order = G.order ↔ SameGroup H G

Under containment, equality of exact orders certifies subgroup equality.

theorem Hex.PermGroup.SameGroup.order_eq {n : Nat} {G H : Group n} (h : SameGroup G H) : G.order = H.order