proposition: Lemma covers_rind (disp : unit) (T : finPOrderType disp) (P : T -> Type) : (forall x y, covers y x -> P x -> P y) -> forall x, P x -> forall y, x >= y -> P y.
proof: Proof. move=> IH x Px y. rewrite -leEdual; apply: covers_ind => // {Px y}x y. by rewrite covers_dual => /IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools