proposition: Lemma lt_succ : forall a, a < succ a.
proof: Proof. intro c; elim c; simpl; auto with T1. intro c0; case c0; simpl; auto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List