proposition: Lemma SF_rev_rcons (s : SF_seq) (t : R*T) : SF_rev (SF_rcons s t) = SF_cons t (SF_rev s).
proof: Proof. apply SF_lx_ly_inj. by rewrite SF_lx_cons !SF_seq_bij_lx SF_lx_rcons rev_rcons. by rewrite SF_ly_cons !SF_seq_bij_ly SF_ly_rcons rev_rcons. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy