proposition: Lemma succ_strict_monoR : forall alpha beta, nf alpha -> nf beta -> lt (succ alpha) (succ beta) -> lt alpha beta.
proof: Proof. intros alpha beta Halpha Hbeta H. apply lt_le_trans with (succ alpha). - now apply lt_succ. - apply lt_succ_le_2; auto. now apply succ_nf. 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)