{x y : No} (p : x < y) : x <= y. Proof. apply No_decode_le. apply lt'_le'. apply No_encode_lt. assumption. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.