proposition: Lemma ex_diff_n_ext_loc: forall f g n x y, locally_2d (fun u v => f u v = g u v) x y -> ex_diff_n f n x y -> ex_diff_n g n x y.
proof: Proof. intros f g n; revert f g. induction n. intros f g x y H; simpl. intros (H1,_); split. apply (continuity_2d_pt_ext_loc _ _ _ _ H H1). easy. simpl. intros f g x y H (H1&H2&H3&H4&H5). split. apply (continuity_2d_pt_ext_loc _ _ _ _ H H1). split. apply: ex_derive_ext_loc H2. apply locally_2d_1d_const_y with (1:=H). split. apply: ex_derive_ext_loc H3. apply locally_2d_1d_const_x with (1:=H). split. apply IHn with (2:=H4). apply locally_2d_impl_strong with (2:=H). apply locally_2d_forall. intros u v H6. apply Derive_ext_loc. apply locally_2d_1d_const_y with (1:=H6). apply IHn with (2:=H5). apply locally_2d_impl_strong with (2:=H). apply locally_2d_forall. intros u v H6. apply Derive_ext_loc. apply locally_2d_1d_const_x with (1:=H6). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive