proposition: Lemma Exercise1_5a r: order r -> order_r (free_subset_compare r).
proof: Proof. move=> or; rewrite /free_subset_compare; split. + move=> x y z [xs ys p1][_ zs p2]; split => //. move=> a ax; move: (p1 _ ax) => [b biy l1]; move: (p2 _ biy) => [c cy l2]. ex_tac; order_tac. + move=> x y [/Zo_P [_ fs1] /Zo_P [_ fs2] p1] [_ _ p2]. set_extens t => ts. move: (p1 _ ts) => [z zy le1]; move:(p2 _ zy) => [w wx le2]. move: (fs1 _ _ ts wx (order_transitivity or le1 le2)) => eq1. by rewrite -eq1 in le2;rewrite (order_antisymmetry or le1 le2). move: (p2 _ ts)=> [z zy le1]; move: (p1 _ zy)=> [w wx le2]. move: (fs2 _ _ ts wx (order_transitivity or le1 le2)) => eq1. by rewrite -eq1 in le2; rewrite (order_antisymmetry or le1 le2). + move=> x y [xs ys p1]; split => //; split =>//a ax; ex_tac; [apply: (Exercise1_5w or xs ax) | apply: (Exercise1_5w or ys ax) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)