(x y : GenNo S) : ((No_raise x <= No_raise y) -> (x <= y)) * ((No_raise x < No_raise y) -> (x < y)). Proof. repeat_No_ind_hprop. destruct (No_raise_cut xL xR xcut) as [rxcut p]; rewrite p. destruct (No_raise_cut xL0 xR0 xcut0) as [rxcut0 q]; rewrite q. split; intros sh. - apply No_encode_le in sh; rewrite le'_cut in sh. apply le_lr. + intros l. apply IHL, No_decode_lt. rewrite q; exact (fst sh l). + intros r. apply IHR0, No_decode_lt. rewrite p; exact (snd sh r). - apply No_encode_lt in sh; rewrite lt'_cut in sh. strip_truncations. destruct sh as [[l sh]|[r sh]]. + apply lt_l with l. apply IHL0, No_decode_le. rewrite p; exact sh. + apply lt_r with r. apply IHR, No_decode_le. rewrite q; exact sh. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.