proposition: Lemma leq_antisym {x y} : x <= y -> y <= x -> x = y.
proof: Proof. intros p q. destruct p. 1: reflexivity. destruct x; [inversion q|]. apply leq_S_n in q. pose (r := leq_trans p q). by apply not_leq_Sn_n in r. Defined.
imports: Basics Types Basics.Nat HoTT.DProp