proposition: Lemma dec_Z_of_pair `{DecidablePaths N} : forall q r : PairT.T N, Decidable (' q = ' r).
proof: Proof. intros q r. destruct (dec (PairT.equiv q r)) as [E|E]. - left. apply Z_path,E. - right. intros E'. apply E. apply (related_path E'). Defined.
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