proposition: Remark Ltb_ij : Nat.ltb i j.
proof: Proof. red; now rewrite Nat.ltb_lt. Defined.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)