proposition: Lemma ishprop_N_lt@{} n m : IsHProp (n < m).
proof: Proof. apply ishprop_sigma_disjoint. intros x y e1 e2. apply N_add_cancel_r with (succ n). rewrite !N_add_succ, <-!N_add_succ_l. path_via m. Qed.
imports: Basics Types HProp PropResizing.PropResizing