proposition: Lemma Ex4_11_minR_P2 R: (forall x, inc x R -> finite_set x) -> (forall P, pure R P <-> pure (min_incl_r R) P).
proof: Proof. move => fr p; split. by move => pr x xp bad; apply: (pr _ xp); move: bad => /Zo_P []. move => pr x xp xR; move: (Ex4_11_minR_pr fr xR) => [y yx ym]. case: (pr _ (sub_trans yx xp) ym). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)