Definition lcoset_in_rcoset_equation {X : gr} {N : subgr X} (H : lcoset_in_rcoset N) (g : X) (n1 : N) : g * (pr1 n1) = (pr1 (lcoset_in_rcoset_witness H g n1)) * g := pr2 (H g n1).
Require Import UniMath.MoreFoundations.Subtypes.