proposition: Lemma uniq_index_not_const : forall n l, uniq (T:=ssrnat_eqType) (index_not_const l n).
proof: Proof. intros n l. unfold index_not_const. apply filter_uniq. apply iota_uniq. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct