Npair_splits@{} : forall n m : N, ' (PairT.C n m) = ' n + - ' m. Proof. intros. apply Z_path;red;simpl. ring_with_nat. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.