proposition: Lemma iorder_gleP r a x y: gle (induced_order r a) x y <-> [/\ inc x a, inc y a & gle r x y].
proof: Proof. split; first by move/setI2_P => [h /setXp_P [pa pb]]. by move => [pa pb pc]; apply /setI2_i => //;apply/setXp_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)