proposition: Lemma Exercise2_3b n (r := opp_order Nat_order) (A := Nint n) (B:= Nat -s A) : natp n -> (order r /\ ex23_prop r A B).
proof: Proof. move=> nN. move: Nat_order_wor => [[o1 _] s1]. move: (opp_osr o1)=> [or]; rewrite s1 => sr. have sAC: sub A (substrate r) by rewrite sr; apply: Nint_S1. move: (iorder_osr or sAC) => [or1 sr1]. move: (complement_p4 sAC) => [p1 p2]. split => //; split => //. - by rewrite /B - sr. - by rewrite /B - sr. - split => //; rewrite sr1. move=> x xA nex; rewrite iorder_trans//. rewrite sr in sAC; move: (@sub_trans _ _ _ xA sAC) => sxB. have p3: (exists n, upper_bound Nat_order x n). have aux: upper_bound Nat_order A n. split; [ue | move=> y; rewrite /A]; move /(NintP nN). move=> [yn _] ; apply /Nat_order_leP;split => //. by apply: (NS_le_nat yn nN). by move: (sub_upper_bound aux xA) => p3; exists n. move: (Nat_greatest sxB nex p3) => [y yg]; exists y. have s2: sub x (substrate Nat_order) by ue. have s3: sub x (substrate r) by ue. move: yg; rewrite /greatest /least ! iorder_sr//. move=> [yx h]; split => // z zx; move: (h _ zx). by move /(iorder_gle0P _ zx yx) /opp_gleP => ha; apply /iorder_gleP. - have bsr: sub B (substrate r) by rewrite sr; apply: sub_setC. case => y [];rewrite iorder_sr//;move=> yb etc. move: (yb) => /setC_P [yB] /(NintP nN) nyn. move: (cltS yB) => [le2 ne1]. have ysB: inc (csucc y) B. apply /setC_P;split; first by apply:NS_succ. move/(NintP nN) =>le1; case: nyn; exact: cle_ltT le2 le1. move: (iorder_gle1 (etc _ ysB)) => /opp_gleP /Nat_order_leP [_ _ le3]. by case: ne1; apply: cleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)