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