(x y : No) : ((x <= y) -> (le' x y)) * ((x < y) -> (lt' x y)). Proof. refine (No_ind_le_lt (fun _ => Unit) (fun x y _ _ _ => le' x y) (fun x y _ _ _ => lt' x y) _ _ _ _ _ x y). + intros; exact tt. + intros; apply path_contr. + intros L R ? xL xR xcut _ _ xcut' L' R' ? yL yR ycut _ _ ycut' xL_lt_y xL_lt_y' x_lt_yR x_lt_yR'. rewrite le'_cut. exact (xL_lt_y' , x_lt_yR'). + intros L R ? xL xR xcut _ _ xcut' L' R' ? yL yR ycut _ _ ycut' l x_le_yL x_le_yL'. rewrite lt'_cut. apply tr; left. exists l. exact x_le_yL'. + intros L R ? xL xR xcut _ _ xcut' L' R' ? yL yR ycut _ _ ycut' r xR_le_y xR_le_y'. rewrite lt'_cut. apply tr; right. exists r. exact xR_le_y'. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.