proposition: Lemma iter_ext l f1 f2 : (forall x, In x l -> f1 x = f2 x) -> iter l f1 = iter l f2.
proof: Proof. elim: l => [ | h l IH] /= Heq. by []. rewrite IH. rewrite Heq //. by left. intros x Hx. apply Heq. by right. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements