proposition: Lemma f_decreases : forall i, f (S i) < f i.
proof: Proof. induction i; compute; auto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List