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