proposition: Theorem termine_gt_compat : termine R.
proof: Proof. red . cut (forall n a, f a < n -> Acc R a). intros H a. apply (H (S (f a))); auto with arith. induction n. intros; absurd (f a < 0); auto with arith. intros a ltSma. apply Acc_intro. intros b ltfafb. apply IHn. assert (f b < f a). apply H_compat. trivial. lia. Qed.
imports: Coq(Lia Relations Wellfounded) CoLoR(term)