proposition: Lemma iorder_gle0P r a x y: inc x a -> inc y a -> (gle (induced_order r a) x y <-> gle r x y).
proof: Proof. move=> xa ya;split;first by case/iorder_gleP. by move => pa; apply /iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)