proposition: Lemma setF_pr A a b: inc A setF -> inc a A -> R a b -> inc b A.
proof: Proof. move /Zo_P => [] /setP_P AE Ap aA Rab. case: (inc_or_not b A)=> // nba. have bc: inc b (E -s A) by apply:setC_i =>//; apply: (A3 (A2 Rab)). by case: (Ap _ _ aA bc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)