proposition: Theorem not_decreasing : ~ (exists f : nat -> A, (forall i:nat, R (f i.+1) (f i))).
proof: Proof. case => f dec. pose p a := Acc R a -> ~ exists i, a = f i. have H: forall a, p a. move => a; apply: (well_founded_ind W p) => x Hx ax [i egi]. move: (dec i); rewrite - egi => H1; move: (Hx _ H1 (acc_rec H1 ax)). by case; exists (i.+1). move: (H _ (W (f 0))); case; by exists 0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)