proposition: Lemma Exercise1_5g r: total_order r -> total_order (free_subset_order r).
proof: Proof. move=> tor; move: (tor)=> [or tr]. have [pa pb] := (fs_order_osr or). split => //; rewrite pb => x y xsf ysf. have ef: (inc emptyset (free_subsets r)). apply: Zo_i; [ by apply:setP_0i | by move=> u _y /in_set0 ]. move: (Exercise1_5e tor xsf) (Exercise1_5e tor ysf) => sx sy. case: (emptyset_dichot x) => xe. rewrite xe; left; apply:Exercise1_5f; fprops. case: (emptyset_dichot y) => ye. rewrite ye; right; apply: Exercise1_5f; fprops. move: xe ye => [X Xx] [Y Yy]. move: xsf ysf => /Zo_P [] /setP_P xsr _/Zo_P [] /setP_P ysr _. move: (xsr _ Xx)(ysr _ Yy) => Xsr Ysr. have ->: (x = singleton X) by apply: set1_pr => // t tx; apply: sx. have ->: (y = singleton Y) by apply: set1_pr => // t tx; apply: sy. by case: (tr _ _ Xsr Ysr) => h; [left | right]; apply/(Exercise1_5cP or). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)