proposition: Lemma lt_succ_le : forall a, nf a -> forall b, nf b -> lt a b -> leq lt (succ a) b.
proof: Proof. induction a. - intros H0 c'; case c'. + intros H1 H2; destruct (not_lt_zero H2). + destruct alpha. * destruct n; intros t H H1; generalize (nf_of_finite H); intro; subst; compute. right; tauto. now left. * intros; simpl. left. compute; tauto. - destruct b. + intros H0 H1; destruct (not_lt_zero H1). + intros H0 H1; destruct (lt_inv H1). * destruct a1; simpl. apply lt_incl_le. auto with T1. apply lt_incl_le. auto with T1. * destruct H2. destruct H2; subst b1. simpl succ. destruct a1. generalize (nf_of_finite H0). intro; subst. red in H3. generalize H3; rewrite Nat.lt_eq_cases. destruct 1 as [H2 | H2]. -- decompose [and] H3; subst. clear H3. simpl succ. left. now apply finite_lt. -- rewrite H2. right. -- destruct (lt_inv H1). left. now apply coeff_lt. destruct H2 as [H2 | H2]. left; now apply coeff_lt. decompose [and] H2; subst. apply le_tail. eauto with T1. -- decompose [and] H2; subst. auto. cbn. destruct b1. ++ generalize (nf_of_finite H0). intro; subst. decompose [and] H2. destruct (not_lt_zero H7). ++ apply le_tail. apply IHa2; eauto with T1. 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)