proposition: Lemma differentiable_pt_lim_unique (f : R -> R -> R) (x y : R) (lx ly : R) : differentiable_pt_lim f x y lx ly -> Derive (fun x => f x y) x = lx /\ Derive (fun y => f x y) y = ly.
proof: Proof. move => Df ; split ; apply is_derive_unique, is_derive_Reals => e He ; case: (Df (pos_div_2 (mkposreal e He))) => {Df} delta /= Df ; exists delta => h Hh0 Hh. replace ((f (x + h) y - f x y) / h - lx) with ((f (x+h) y - f x y - (lx * ((x+h) - x) + ly * (y - y))) / h) by (by field). rewrite Rabs_div. apply Rlt_div_l. by apply Rabs_pos_lt. apply Rle_lt_trans with (e / 2 * Rmax (Rabs (x + h - x)) (Rabs (y - y))). apply (Df (x+h) y). by (ring_simplify (x + h - x)). rewrite Rminus_eq_0 Rabs_R0 ; by apply delta. ring_simplify (x + h - x). rewrite Rmax_left. apply Rmult_lt_compat_r. by apply Rabs_pos_lt. lra. rewrite Rminus_eq_0 Rabs_R0 ; by apply Rabs_pos. by []. replace ((f x (y + h) - f x y) / h - ly) with ((f x (y + h) - f x y - (lx * (x - x) + ly * ((y + h) - y))) / h) by (by field). rewrite Rabs_div. apply Rlt_div_l. by apply Rabs_pos_lt. apply Rle_lt_trans with (e / 2 * Rmax (Rabs (x - x)) (Rabs (y + h - y))). apply (Df x (y + h)). rewrite Rminus_eq_0 Rabs_R0 ; by apply delta. by (ring_simplify (y + h - y)). ring_simplify (y + h - y). rewrite Rmax_right. apply Rmult_lt_compat_r. by apply Rabs_pos_lt. lra. rewrite Rminus_eq_0 Rabs_R0 ; by apply Rabs_pos. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive