proposition: Lemma Exercise1_22C F U U': cofinal r F -> open_r r U -> open_r r U' -> sub (U \cap F) (U' \cap F) -> sub U U'.
proof: Proof. move=> [cf1 cfi] oU oU' sUU'. move: (oU) => [[sU sU1] _]. move=> t tU; rewrite(Exercise1_22p oU'); apply: Exercise1_22h; fprops. by case: oU'. move=> y ty. have ysr: (inc y (substrate r)) by order_tac. move: (cfi _ ysr) => [z zF yz]. move: (sU1 _ _ tU (order_transitivity or ty yz)) => zU. have zi: inc z (U' \cap F) by apply:sUU'; apply:setI2_i =>//. move: (setI2_1 zi) => zU'; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)