proposition: Lemma Exercise1_23j r: order r -> let r':= nregs_order r in (forall x y, inc x (substrate r') -> inc y (substrate r') -> ( (forall z, gle r' x z -> gle r' y z -> False) <-> (disjoint x y))).
proof: Proof. move=> or r' x y xsr' ysr'. move:(sub_osr (nreg_opens r)) => [pr1 pr2]. move: (opp_osr pr1) => [or' prb]. have sr': (substrate r' = nreg_opens r) by rewrite /r' prb pr2. rewrite /r'/nregs_order; aww. split. move=> h; apply: disjoint_pr=> u ux uy. rewrite sr' in xsr' ysr'. exact (h _ (Exercise1_23i or ux xsr') (Exercise1_23i or uy ysr')). rewrite /disjoint=> di z => /(Exercise1_23bP or) [_ [t tz] _ _ zx] /(Exercise1_23bP or) [_ _ _ _ zy]. empty_tac1 t; apply: setI2_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)