proposition: Lemma terminates_gtn : terminates (fun n m => m < n).
proof: Proof. move => n. elim: n {-2}n (leqnn n) => [|n IHn] m Hm ;constructor. - move => k Hk. by move: (leq_trans Hk Hm). - move => k Hk. apply: IHn. rewrite -ltnS. exact: leq_trans Hm. Qed.
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)