{x y z : No} : (x < y) -> (y <= z) -> (x < z). Proof. intros p q. apply No_decode_lt. refine (lt_le'_trans x y z p _). apply No_encode_le. assumption. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.