proposition: Lemma size_ind (X : Type) (f : X -> nat) (P : X -> Type) : (forall x, (forall y, (f y < f x) -> P y) -> P x) -> forall x, P x.
proof: Proof. move => ind x; have [n] := ubnP (f x); elim: n x => // n IHn x le_n. apply: ind => y f_y_x; apply: IHn; exact: leq_trans f_y_x _. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)