proposition: Lemma ordering_pair3 x y : ord_pair_le x y -> inc x (coarse (osucc (ord_pair_max y))).
proof: Proof. move=> [px py le]; apply /setX_P. move: (ordering_pair2 py) => oo; move: (OS_succ oo) => soo. set t := (osucc (ord_pair_max y)). suff: inc (P x) t /\ inc (Q x) t by move =>[pa pb];split=> //;case:px. case: le => [][le aux]. case: (ordering_pair1 px); move => [pa pb]; rewrite pb in le; split;apply /(oltP soo); apply /oltSleP => //; apply:(oleT pa le). case: (ordering_pair1 px); move=> [pa pb]; split;apply /(oltP soo); apply /oltSleP => //; rewrite -le pb => //;apply:(oleR (proj32 pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)