proposition: Lemma ap_plusR : forall c, nf c -> c <> zero -> (forall a b, nf a -> nf b -> lt a c ->lt b c -> lt (a + b) c) -> ap c.
proof: Proof. destruct c as [|c1 n c2]. - now destruct 2. - case c2. + case n. * constructor. * intros n0 H H0 H1; generalize (H1 (cons c1 0 zero) (cons c1 n0 zero)). clear H1;intros H1. assert (H2 : nf (cons c1 0 zero)) by (eapply nf_coeff_irrelevance;eauto). assert (H3 : nf (cons c1 n0 zero)) by (eapply nf_coeff_irrelevance;eauto). assert (H4 : lt (cons c1 0 zero) (cons c1 (S n0) zero)). { auto with T1 arith. } assert (H5 : lt (cons c1 n0 zero) (cons c1 (S n0) zero )) by (auto with T1 arith ). generalize (H1 H2 H3 H4 H5); intro H6. rewrite plus_cons_cons_rw2 in H6; simpl in H6. 2-3: auto. now apply lt_irrefl in H6. + intros t n0 t0 H H0 H1; assert (H2 : nf (cons c1 n zero)). { apply single_nf; eapply nf_inv1; eauto. } assert (H3: nf (cons t n0 t0)). { eapply nf_inv2; eauto. } assert (H4 : lt (cons c1 n zero) (cons c1 n (cons t n0 t0))). { apply tail_lt; auto with T1. } assert (H5 : lt (cons t n0 t0) (cons c1 n (cons t n0 t0))). { apply nf_inv3 in H. auto with T1. } generalize (H1 _ _ H2 H3 H4 H5). clear H1 H4 H5;intro H1; rewrite plus_cons_cons_rw3 in H1; auto. * simpl in H1; now apply lt_irrefl in H1. * apply nf_inv3 in H; auto. 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)