proposition: Lemma wf_leq X (f : X -> nat) : well_founded (fun x y => f x < f y).
proof: Proof. by apply: (@Wf_nat.well_founded_lt_compat _ f) => x y /ltP. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)