proposition: Lemma finite_ltR : forall n p : nat, lt (FS n) (FS p) -> (n < p)%nat.
proof: Proof. intros; simpl in H. unfold lt in H. destruct (compare _ _) eqn:?. 1,3: easy. unfold compare in Heqc; simpl in Heqc. destruct (n ?= p) eqn:?. 1,3: easy. now apply Nat.compare_lt_iff. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)