proposition: Lemma index_not_const_correct : forall n l (k : nat), not (in_mem k (mem (index_not_const l n))) -> is_const (nth (Cst 0) l k) n = true.
proof: Proof. intros n l k. rewrite /index_not_const (@mem_filter ssrnat_eqType) mem_iota /=. rewrite ssrnat.add0n. case E: ssrnat.leq. case is_const. easy. now elim. intros _. rewrite nth_default //. revert E. rewrite ssrnat.ltnNge. now case ssrnat.leq. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct