proposition: Lemma proper_ind (T: finType) (P : pred T -> Type) : (forall A : pred T, (forall B : pred T, B \proper A -> P B) -> P A) -> forall A, P A.
proof: Proof. move => ind; elim/card_ind => A IH. apply: ind => B /proper_card; exact: IH. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)