proposition: Lemma SF_rev_inj (s s0 : SF_seq) : SF_rev s = SF_rev s0 -> s = s0.
proof: Proof. move => H ; by rewrite -(SF_rev_invol s) -(SF_rev_invol s0) H. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy