proposition: Lemma nat_size_ind (X:Type) (P : X -> Type) (f : X -> nat) : (forall x, (forall y, (f y < f x) -> P y) -> P x) -> forall x, P x.
proof: Proof. move => H. apply: well_founded_induction_type; last exact H. exact: wf_leq. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)