proposition: Lemma SF_rev_invol (s : SF_seq) : SF_rev (SF_rev s) = s.
proof: Proof. apply SF_lx_ly_inj. by rewrite /SF_rev ?SF_seq_bij_lx revK. by rewrite /SF_rev ?SF_seq_bij_ly revK. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy