proposition: Lemma IFE_gltP x y: glt IFS_order x y <-> [/\ inc x IFSE, inc y IFSE & IFS_order_rel x y].
proof: Proof. split. by move => [/graph_on_P1 [xe ye ha] hb]; case: ha. move => [ha hb hc]; split. by apply/graph_on_P1; split => //; right. move => xy; case: hc; rewrite xy. - by move => /proj2; case. - by move => [_ /proj2]. - by move => [_ _ /proj2]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)