proposition: Lemma Exercise6_31_i: order_on r' F.
proof: Proof. move: Exercise6_31_a =>[or sr]. have ha: sub count_inf_subsets (substrate r) by rewrite sr; apply: Zo_S. exact: (iorder_osr or ha). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)