proposition: Lemma interp_ext : forall l1 l2 e, (forall k, nth 0 l1 k = nth 0 l2 k) -> interp l1 e = interp l2 e.
proof: Proof. intros l1 l2 e Hl. revert l1 l2 Hl. induction e using expr_ind'. now simpl => l1 l2 Hl. simpl => l1 l2 Hl. apply apply_ext. intros n _. revert n. induction le. easy. simpl in H |- *. destruct H as (Ha,Hb). intros [|n]. simpl. now apply Ha. now apply IHle. simpl => l1 l2 Hl. unfold Derive_Rn. assert (Hn: forall n, nth 0 (map (interp l1) le) n = nth 0 (map (interp l2) le) n). intros p. rewrite (nth_map' (Cst 0) (interp l1)) (nth_map' (Cst 0) (interp l2)). now apply (foldr_prop_nth _ _ _ H). rewrite Hn. apply Derive_ext => t. apply apply_ext => p Hp. now rewrite Hn. simpl => l1 l2 Hl. apply IHe1. intros [|k]. now apply IHe2. apply Hl. intros l1 l2 Hl. rewrite /interp -/interp. apply IHe1 => k. rewrite 2!nth_set_nth /=. case eqtype.eq_op. now apply IHe2. apply Hl. easy. simpl => l1 l2 Hl. apply f_equal2. now apply IHe1. now apply IHe2. simpl => l1 l2 Hl. apply f_equal. now apply IHe. simpl => l1 l2 Hl. rewrite (IHe2 l1 l2 Hl) (IHe3 l1 l2 Hl). apply RInt_ext => x _. apply IHe1. intros [|k]. easy. apply Hl. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct