Definition rcoset_in_lcoset_equation {X : gr} {N : subgr X} (H : rcoset_in_lcoset N) (g : X) (n1 : N) : (pr1 n1) * g = g * (pr1 (rcoset_in_lcoset_witness H g n1)) := pr2 (H g n1).
Require Import UniMath.MoreFoundations.Subtypes.