proposition: Lemma Exercise6_9a n: natp n -> (Nint_co n = induced_order Nat_order (segment Nat_order n)).
proof: Proof. move =>nN; rewrite segment_Nat_order //. move : Nat_order_wor => [[o2 _] sb]. move: (Nintco_wor n) => [o1 _]. rewrite -/(Nint n). move: (@Nint_S1 n); rewrite - sb => si. move: (iorder_osr o2 si)=> [o3 sr3]. rewrite -/(Nint n); apply: order_exten => //; first by fprops. move=> x y; split. move => h; move /(Nintco_gleP nN):(h) => [pa pb]. move: h => /Zo_P [] /setXp_P [xi yi] _. move: (xi) (yi) => /Zo_P [xsr _] /Zo_P [ysr _]. apply/iorder_gle0P => //;apply /Nat_order_leP; split =>//; rewrite /natp; ue. move /iorder_gleP => [pa pb] /Nat_order_leP [pc pd pe]. by apply /(Nintco_gleP nN);split => //; apply /(NintP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)