proposition: Lemma Exercise2_7A5 f (g:= extension_to_NNstar f) (E:= substrate NNstar): function_prop f Nat Nat -> [/\ (forall x, natp x -> Vf g (J x C0) = (J (Vf f x) C0)), (forall x, inc x E -> Q x = C0 -> (P (Vf g x) = Vf f (P x) /\ Q (Vf g x) = C0)), (forall x, inc x E -> Q x <> C0 -> Vf g x = x) & function_prop g E E].
proof: Proof. move=> [ff sf tf]. move: Exercise2_7A3 => [[_ ss] _]. have ta:(lf_axiom (fun z=> Yo (Q z = C0) (J (Vf f (P z)) C0) z) (canonical_du2 Nat Nat) (canonical_du2 Nat Nat)). move: C1_ne_C0 => tpd. move=> t /candu2P. move=> [pt]; case; move=> [Pt Qt]; rewrite Qt; Ytac0. apply: candu2_pra; Wtac. by rewrite - pt Qt; apply: candu2_prb. rewrite /g /extension_to_NNstar /E ss. split => //. move=> x xB; rewrite LfV//; aw; [by Ytac0 | by apply: candu2_pra]. move=> x xE; rewrite LfV//; move=> ->; Ytac0; saw. move=> x xE; rewrite LfV//; move=> h; Ytac0; fprops. by red; saw; apply: lf_function. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)