proposition: Theorem orderP r: order r <-> (r \cg r = r /\ r \cap (opp_order r) = diagonal (substrate r)).
proof: Proof. split. move=> or. set (d:= diagonal (substrate r)). have i2: (r \cap (opp_order r) = d). set_extens t. move /setI2_P => [tr /igraphP [pt Jr]]. apply /diagonal_i_P;split => //; first by substr_tac. rewrite -pt in tr; apply: (order_antisymmetry or tr Jr). move/diagonal_i_P => [pt Ps pq]. rewrite -pt -pq. have rpp: (related r (P t) (P t)) by order_tac. by apply: setI2_i=>//; apply/igraph_pP. have gr: (sgraph r) by fprops. have sd: (sub d r) by rewrite -i2; apply : setI2_1. have sc: (sub (d \cg r) (r \cg r)) by apply: compg_S; fprops. have crrr: (sub (r \cg r) r). move: or => [_ _ t _];rewrite -idempotent_graph_transitive //. by split =>//; apply: preorder_prop1. move=> [crrr iro]. have sr: sgraph r by rewrite -crrr; apply: compg_graph. split=> //. - move=> y ys. have: (inc (J y y) (diagonal (substrate r))) by apply /diagonal_pi_P. by rewrite -iro; move=> Ji; apply: (setI2_1 Ji). - have: sub (r \cg r) r by rewrite crrr; fprops. rewrite -idempotent_graph_transitive //. - move => x y rxy ryx. have p1: (inc (J x y) (opp_order r)) by apply/igraph_pP. have: (inc (J x y) (diagonal (substrate r))). by rewrite - iro; apply: setI2_i. by move /diagonal_pi_P => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)