proposition: Lemma Exercise1_5cP r x y: order r -> inc x (substrate r) -> inc y (substrate r) -> (gle r x y <-> gle (free_subset_order r) (singleton x) (singleton y)).
proof: Proof. move => or xsr ysr. split. move => lxy; apply /fs_order_gleP; split => //; try apply: Exercise1_5b => //. move => u /set1_P ->; exists y; fprops. by move /fs_order_gleP => [_ _ rxy];move:(rxy _ (set1_1 x)) => [z] /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)