fact: Definition Z_rect@{i} (P : Z -> Type@{i}) {sP : forall x, IsHSet (P x)} (dclass : forall x : PairT.T N, P (' x)) (dequiv : forall x y E, (Z_path E) # (dclass x) = (dclass y)) : forall q, P q := quotient_ind PairT.equiv P dclass dequiv.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals