{G : Group} {N : NormalSubgroup G} (x x' y y' : G) : in_cosetR N x y -> in_cosetR N x' y' -> in_cosetR 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. 2: exact q. apply isnormal. exact p. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.