proposition: Lemma grlcan (X : gr) {a b : X} (c : X) (e : paths (op c a) (op c b)) : a = b.
proof: Proof. apply (invmaponpathsweq (weqlmultingr X c) _ _ e). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids