proposition: Lemma fs_order_osr r: order r -> order_on (free_subset_order r) (free_subsets r).
proof: Proof. move=> or; red;rewrite /free_subset_order graph_on_sr //. split => //; apply: order_from_rel; apply: Exercise1_5a =>//. move => a ax; split => // t ts;ex_tac; apply: (Exercise1_5w or ax ts). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)