proposition: Lemma terminates_measure T (f : T -> nat) (e : T -> T -> Prop) : (forall x y, e x y -> f y < f x) -> terminates e.
proof: Proof. move => H x. exact: sn_preimage (terminates_gtn (f x)). Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)