proposition: Lemma fs_order_gleP r x y: gle (free_subset_order r) x y <-> free_subset_compare r x y.
proof: Proof. split; first by move /Zo_hi; aw. move =>h; apply: Zo_i; last by aw. by move: h => [pa pb _]; apply :setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)