proposition: Lemma finord_wf (disp : unit) (T : finPOrderType disp) (P : T -> Type) : (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.
proof: Proof. move=> IH x. have [n] := ubnP #|[set y : T | y < x]|; elim: n => // n IHn in x *. rewrite ltnS leq_eqVlt; case: eqP => [eqcn _ | _ ]; last exact: IHn. apply: IH => y ltxy; apply: IHn. rewrite -{}eqcn; apply proper_card; apply/andP; split; apply/subsetP. - by move=> z; rewrite !inE => /lt_trans; apply. - by move/(_ y); rewrite !inE => /(_ ltxy); rewrite ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools