proposition: Lemma lt_succ_succ : forall a b, a < b -> nf a -> nf b -> succ a < succ b.
proof: Proof. induction 1. simpl. case a. constructor 3;auto with arith. constructor 2. constructor. generalize H; simpl. case a. case a'. inversion 1. constructor 2. constructor 1. case a'. inversion 1. constructor 2;auto. simpl. case a. constructor 3;auto with arith. constructor 3;auto. simpl. case a. intros. assert (b'=zero). inversion H1. auto. inversion H5. subst b';inversion H. constructor 4. apply IHlt; nf_inv. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List