proposition: Lemma covers_ind (P : T -> Type) : (forall x y, covers x y -> P x -> P y) -> forall x, P x -> forall y, x <= y -> P y.
proof: Proof. move=> IH x Px; elim/finord_wf => y IHy. rewrite le_eqVlt; case: eqP => [<-|] //= _ ltxy. case: (boolP (covers x y)) => [/IH|]; first exact. rewrite /covers /= ltxy /= -negb_exists negbK => /existsP/sigW [z0]. move/(arg_minP (P := [pred z | x < z < y]) (fun z => #|[pred t | z < t < y]|)) => {z0} [zmin /andP[ltxz ltzy] Hzmin]. suff /IH : covers zmin y by apply; apply: (IHy _ ltzy (ltW ltxz)). rewrite /= ltzy /=; apply/forallP => u; apply/negP => /andP[ltzu ltuy]. have /Hzmin : x < u < y by rewrite ltuy (lt_trans ltxz ltzu). rewrite leNgt => /negP; apply. apply proper_card; rewrite /= properE; apply/andP; split. by apply/subsetP => v; rewrite !unfold_in => /andP[/(lt_trans ltzu)->->]. apply/negP => /subsetP/(_ u); rewrite !unfold_in ltxx /= => Habs. by have /Habs : zmin < u < y by rewrite ltzu ltuy. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools