proposition: Lemma Exercise6_31_j x y: gle r' x y <-> [/\ inc x F, inc y F & sub y x].
proof: Proof. apply: (iff_trans (iorder_gleP r F x y)). split; move =>[xF yF etc]; split => //. by case/Exercise6_31_b: etc. apply/Exercise6_31_b; split; [apply: (Zo_S xF) | apply: (Zo_S yF) | done ]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)