fact: Definition No_ind_package : { f : forall x, A x & (forall (x y : GenNo) (p : x <= y), dle x y p (f x) (f y)) * (forall (x y : GenNo) (p : x < y), dlt x y p (f x) (f y)) } := ( No_ind ; (No_ind_le , No_ind_lt) ).
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core