{G : Group} {N : NormalSubgroup G} (x x' y y' : G) : in_cosetL N x y -> in_cosetL N x' y' -> in_cosetL N (x * x') (y * y'). Proof. cbn; intros p q. rewrite negate_sg_op, <- simple_associativity. apply isnormal. rewrite simple_associativity, <- simple_associativity. apply subgroup_in_op. 1: exact p. apply isnormal. exact q. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.