proposition: Lemma SF_seq_bij_ly (lx : seq R) (ly : seq T) (Hs : size lx = S (size ly)) : SF_ly (SF_make lx ly Hs) = ly.
proof: Proof. case: lx Hs => // x lx Hs ; rewrite /SF_make / SF_ly unzip2_zip //= ; apply SSR_leq, le_S_n ; rewrite -Hs => //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy