proposition: Lemma lt_n_Sn@{} n : lt n (S n).
proof: Proof. constructor. revert n. apply nat_rect@{Set}; intros; now constructor. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded HoTT(Spaces.Nat)