proposition: Lemma iscontr_affine_line (T:Torsor ℤ) : iscontr (affine_line T).
proof: Proof. intros. apply iscontraprop1. { apply propproperty. } exact (torsor_nonempty T). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.MoreEquivalences UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.GroupAction UniMath.NumberSystems.Integers