proposition: Lemma Exercise1_5f r X Y: order r -> inc X (free_subsets r) -> inc Y (free_subsets r) -> sub X Y -> gle (free_subset_order r) X Y.
proof: Proof. move=> or Xsf Ysf XY; apply /fs_order_gleP; split => //. move=> x xX;move: (XY _ xX) => xY; ex_tac; apply: (Exercise1_5w or Ysf xY). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)