fact: Definition No_ind_le_lt (x y : GenNo) : (forall (p : x <= y), dle x y p (No_ind x) (No_ind y)) * (forall (p : x < y), dlt x y p (No_ind x) (No_ind y)) := (No_ind_le x y , No_ind_lt x y).
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core