proposition: Lemma Exercise2_5 r: order r -> inductive r -> has_greatest (free_subset_order r).
proof: Proof. move=> or isr;set (A:= Zo (substrate r) (maximal r)). have fs: (free_subset r A). by move => x y => /Zo_hi [_ xm] _ xy; rewrite (xm _ xy). have Af:(inc A (free_subsets r)) by apply: Zo_i => //; apply /setP_P; apply: Zo_S. move: (fs_order_osr or) => [fso fsr]. exists A; split; first by ue. rewrite fsr => x xs; apply /fs_order_gleP; split => //. move=> y yx. move:xs =>/Zo_P [] /setP_P xsr _. move: (inductive_max_greater or isr (xsr _ yx)) => [m [mm ym]]. exists m => //; apply: Zo_i => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)