proposition: Lemma plus_a_zero : forall a, nf a -> a + zero = a.
proof: Proof. intro c; case c;simpl. trivial. intro c0;case c0;simpl;auto. intros n c1 H1; rewrite (nf_of_finite H1); auto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List