proposition: Lemma total_orderP r: total_order r <-> [/\ r \cg r = r, r \cap (inverse_graph r) = diagonal (substrate r)& r \cup (inverse_graph r) = coarse (substrate r) ].
proof: Proof. rewrite /total_order. split. move=> [or to]; move /orderP: (or) => [p1 p2]. split => //; set_extens x => xu. case /setU2_P: xu. have gr: (sgraph r) by fprops. apply: (sub_graph_coarse_substrate gr). have [oor sor] := (opp_osr or). have gr: sgraph (opp_order r) by fprops. by rewrite - sor; apply: (sub_graph_coarse_substrate gr). move: xu => /setX_P [ px Ps Qs]; rewrite - px. by case:(to _ _ Ps Qs)=> xx;apply/setU2_P;[ by left | right; apply/igraph_pP]. move=> [cg i2 u2]. have or :order r by apply/orderP. split=>// x y xs ys. have Jc: inc (J x y) (coarse (substrate r)) by apply/setXp_P; split. move: Jc; rewrite -u2;case /setU2_P=> xx; [by left | right]. by apply/igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)