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