proposition: Lemma Exercise2_7A6: forall f, closure f Nat_order -> closure (extension_to_NNstar f) NNstar.
proof: Proof. move=> f [ [ob _ [ff sf tf] incf] c1 c2]. move: (proj2 Nat_order_wor) => bos. have fp: function_prop f Nat Nat by split => //; ue. move: (Exercise2_7A5 fp). set g:= (extension_to_NNstar f); set (E:=substrate NNstar). move=> [ga0 ga gb [fg sg tg]]. move: Exercise2_7A3 => [[oNN sNN] leNNP]. rewrite /E sNN in sg tg ga gb. split. split;fprops; first by saw; ue. move=> x y =>/leNNP [p1 p2 p3]; apply /leNNP; split; try Wtac. case: p3. move=> [q1 q2 q3]; constructor 1. move: (ga _ p1 q1) (ga _ p2 q2) => [r1 r2] [r3 r4]. rewrite r1 r2 r3 r4; split => //. have aux: gle Nat_order (P x) (P y). apply /Nat_order_leP => //; split => //. by move:p1 => /candu2P [ _ ]; case; move=> [px qx]. by move:p2 => /candu2P [ _ ]; case; move=> [px qx]. by move: (incf _ _ aux) => /Nat_order_leP [_ _]. move=> [q1 q2 q3]; constructor 2. by move: (gb _ p1 q1) (gb _ p2 q2) => -> ->. move=> [q1 q2]; constructor 3. by move: (ga _ p1 q1) (gb _ p2 q2) => [_] -> ->. rewrite sNN; move=> x xs; apply /leNNP; split => //. rewrite -tg; apply: Vf_target=> //; ue. move: (xs) =>/candu2P [ _ ]; case. move=> [pb qx]; move: (ga _ xs qx); move=> [pw qw]; constructor 1. rewrite pw qw;split => //; rewrite bos in c1; move: (c1 _ pb). by move /Nat_order_leP => [_ _]. move=> [pb qx]; have qqx: (Q x <> C0) by rewrite qx; fprops. move: (gb _ xs qqx) => ->; constructor 2; split;fprops. move=> x; rewrite sNN => xs. move: (xs) => /candu2P [ _ ]; case. move=> [px qx]; move: (ga _ xs qx) ; move=> [pw qw]. have wa: inc (Vf g x) (canonical_du2 Nat Nat). rewrite -tg; apply: Vf_target => //; ue. move: (ga _ wa qw) ; move=> [pw2 qw2]. have wb: inc (Vf g (Vf g x)) (canonical_du2 Nat Nat) by Wtac. move: wa => /candu2P [pw3 _ ]. move: wb =>/candu2P [pw4 _ ]. apply: pair_exten => //; [ rewrite pw2 pw c2 //; ue | rewrite qw2 //]. move=> [_ qx]; have qqx: (Q x <> C0) by rewrite qx; fprops. by move: (gb _ xs qqx) => aux; rewrite {1} aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)