proposition: Lemma fact5 (X: Torsor ℤ) (x:X) : loop @ s x = s (transportf elem (loop' X) x).
proof: Proof. refine (_ @ !fact2 x). exact (fact4 x). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Equivalences UniMath.MoreFoundations.PathsOver UniMath.Algebra.Monoids UniMath.SyntheticHomotopyTheory.AffineLine UniMath.NumberSystems.Integers UniMath.Algebra.BinaryOperations UniMath.Algebra.GroupAction UniMath.Algebra.Groups