proposition: Lemma Exercise4_6a: order_on E46_order_r E46_u /\ (forall x y, gle E46_order_r x y <-> [/\ inc x E46_u, inc y E46_u & E46_order_rel x y]).
proof: Proof. have pa: (forall a, inc a E46_u -> E46_order_rel a a). by move => a _; left. move: (graph_on_sr pa); rewrite -/E46_order_r => sr. have or: order E46_order_r. apply: order_from_rel;split => //. move=> y x z; case => xy; first (by rewrite xy); case => yz => //. by rewrite -yz; right. move: xy yz => [_ yY _][yX _ _];empty_tac1 y. move => x y; case => // xy; case => // yx. move: xy yx => [_ yY _][yX _ _]; empty_tac1 y. by move => x y _; split; left. split => //; move=> x y; apply /graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)