proposition: Lemma propers_ind (T: finType) (P : {set T} -> Type) : (forall A : {set T}, (forall B : {set 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)