proposition: Lemma lt_succ_le_2 : forall a, nf a -> forall b, nf b -> lt a (succ b) -> leq lt a b.
proof: Proof. intros c Hc; elim Hc using nf_rect. - intros;apply zero_le. - intros n b H; case b; cbn. + intros H0; generalize (lt_inv_coeff_dec H0). intros [H2 | [_ H2]]; inversion H2. + destruct alpha. * intros. destruct (lt_inv_coeff_dec H0). assert (H8:n = n0 \/ (n < n0)%nat) by lia. destruct H8. destruct beta. subst n0. auto with T1. subst n0; auto with T1. auto with T1. left. apply coeff_lt. auto. destruct a as [_ H2]; destruct (not_lt_zero H2). * intros. apply lt_incl_le. auto with T1. - destruct b0. intros. cbn in H5. destruct (lt_inv H5). destruct (not_lt_zero H6). destruct H6. destruct H6; discriminate. destruct H6; discriminate. intros. cbn in H5. destruct b0_1. destruct (lt_inv H5). destruct (not_lt_zero H6). destruct H6; discriminate. destruct (lt_inv H5). apply lt_incl_le;auto with T1. destruct H6. destruct H6. injection H6;intros. subst. auto with T1. clear H6. left. now apply coeff_lt. decompose [and] H6. injection H7; intros; subst. apply le_tail. apply H3; trivial. now apply nf_inv2 in H4. 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)