proposition: Lemma apply_ext : forall T k (f : Rn k T) g1 g2, (forall n, (n < k)%nat -> g1 n = g2 n) -> apply k f g1 = apply k f g2.
proof: Proof. intros T k f g1 g2 Hg. revert f. induction k. easy. simpl. intros f. rewrite Hg. apply IHk. intros n Hn. apply Hg. now apply Nat.lt_lt_succ_r. apply Nat.lt_succ_diag_r. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct