proposition: Lemma iorder_trans a b c: sub c b -> induced_order (induced_order a b) c = induced_order a c.
proof: Proof. move=> cb; rewrite /induced_order. have scc: (sub (coarse c) (coarse b)) by apply:setX_Sll. by rewrite - setI2_A; congr intersection2; apply/setI2id_Pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)