Apart (T N) := fun a b => apart (pos a + neg b) (pos b + neg a). Global Instance Tle_hprop@{} : is_mere_relation (T N) Tle. Proof. intros;unfold Tle. apply full_pseudo_srorder_le_hprop. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.