proposition: Lemma ap_plusR : forall c, nf c -> c <> zero -> (forall a b, nf a -> nf b -> a < c -> b < c -> a + b < c) -> ap c.
proof: Proof. destruct c. intros; absurd (zero = zero); auto. case c2. case n. constructor. intros. generalize (H1 (cons c1 0 zero) (cons c1 n0 zero)). clear H1;intros. assert (nf (cons c1 0 zero)). eapply nf_coeff_irrelevance;eauto. assert (nf (cons c1 n0 zero)). eapply nf_coeff_irrelevance;eauto. assert (lt (cons c1 0 zero) (cons c1 (S n0) zero)). constructor 3;auto with arith. assert (lt (cons c1 n0 zero) (cons c1 (S n0) zero) ). constructor 3;auto with arith. generalize (H1 H2 H3 H4 H5). intro. rewrite plus_cons_cons_rw2 in H6. simpl in H6. case (lt_irr H6). auto. auto. intros. assert (nf (cons c1 n zero)). constructor. nf_inv. assert (nf (cons t n0 t0)). nf_inv. assert (cons c1 n zero < cons c1 n (cons t n0 t0)). constructor 4;auto with T1. assert (lt (cons t n0 t0) (cons c1 n (cons t n0 t0))). constructor 2. inversion H;auto. generalize (H1 _ _ H2 H3 H4 H5). clear H1 H4 H5;intro. rewrite plus_cons_cons_rw3 in H1. simpl in H1. case (lt_irr H1). inversion H;auto. auto. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List