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