proposition: Lemma Exercise1_5w r x a: order r -> inc x (free_subsets r) -> inc a x -> gle r a a.
proof: Proof. by move=> or xr ax; order_tac;move: xr => /Zo_P [] /setP_P xsr _; apply: xsr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)