proposition: Lemma contraction_fixpoint_unique {R : realDomainType} {X : normedModType R} (U : set X) (f : {fun U >-> U}) (x y : X) : is_contraction f -> U x -> U y -> x = f x -> y = f y -> x = y.
proof: Proof. case => q [q1 ctrfq] Ux Uy fixx fixy; apply/subr0_eq/normr0_eq0/eqP. have [->|xyneq] := eqVneq x y; first by rewrite subrr normr0. have xypos : 0 < `|x - y| by rewrite normr_gt0 subr_eq0. suff : `|x - y| <= q%:num * `|x - y| by rewrite ler_pMl // leNgt q1. by rewrite [in leLHS]fixx [in leLHS]fixy; exact: (ctrfq (_, _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule