(x y : No) : ((le' x y) -> (x <= y)) * ((lt' x y) -> (x < y)). Proof. revert x y. refine (No_ind_hprop _ _); intros L R ? xL xR xcut xHL xHR. nrefine (No_ind_hprop _ _). { intro x; nrapply istrunc_prod; nrapply istrunc_arrow; exact _. } intros L' R' ? yL yR ycut yHL yHR. split. - intros x_le_y. rewrite le'_cut in x_le_y. exact (le_lr xL xR xcut yL yR ycut (fun l => snd (xHL l _) (fst x_le_y l)) (fun r => snd (yHR r) (snd x_le_y r))). - intros x_lt_y. rewrite lt'_cut in x_lt_y. strip_truncations; destruct x_lt_y as [[l x_le_yL]|[r xR_le_y]]. + apply lt_l with l. exact (fst (yHL l) x_le_yL). + apply lt_r with r. exact (fst (xHR r _) xR_le_y). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.