proposition: Lemma Exercise6_31_b x y: gle r x y <-> [/\ inc x inf_subsets, inc y inf_subsets & sub y x].
proof: Proof. apply: (iff_trans (opp_gleP (sub_order inf_subsets) x y)). apply: (iff_trans (sub_gleP inf_subsets y x)). by split => - [qa qb qc]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)