proposition: Lemma iorder_equivalence r x: sub x (substrate r) -> equivalence r -> equivalence (induced_order r x).
proof: Proof. move => sxr [qa qb qc qd]. split => //. - by move => a /setI2_P/proj2/setX_P/proj31. - move => a asr. suff ax: inc a x by apply/iorder_gleP; split => //; apply: qb; apply: sxr. by case /setU2_P: asr => /funI_P [z /setI2_P [zr /setX_P [za zb zc]] ->]. - move => b a c /iorder_gleP [ax bx ha] /iorder_gleP[_ cx hb]. apply/ iorder_gleP; split => //; apply: qc ha hb. - move => a b /iorder_gleP [ax bx ha]; apply /iorder_gleP; split => //. by apply: qd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)