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