proposition: Lemma finord_wf_down (disp : unit) (T : finPOrderType disp) (P : T -> Type) : (forall x, (forall y, y > x -> P y) -> P x) -> forall x, P x.
proof: Proof. exact: (finord_wf (T := T^d : finPOrderType _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools