proposition: Lemma SF_seq_bij (s : SF_seq) : SF_make (SF_lx s) (SF_ly s) (SF_size_lx_ly s) = s.
proof: Proof. case: s => sh st ; by rewrite /SF_make (zip_unzip st). Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy