proposition: Lemma Exercise1_5h r: order r -> total_order (free_subset_order r) -> total_order r.
proof: Proof. move=> or tor; split => // x y xsr ysr. move: tor => [_]; rewrite (proj2 (fs_order_osr or)) => h. by case: (h _ _ (Exercise1_5b or xsr) (Exercise1_5b or ysr)) => h1; [left | right];apply/Exercise1_5cP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)