proposition: Lemma SF_rev_f2 {T : Type} (f2 : R -> R -> T) P : (forall x y, f2 x y = f2 y x) -> SF_rev (SF_seq_f2 f2 P) = SF_seq_f2 f2 (rev P).
proof: Proof. move => Hf2 ; apply SF_lx_ly_inj ; case: P => [ | h P] //=. rewrite SF_lx_rev !SF_lx_f2 ?rev_cons /= 1?headI // ; by apply Nat.lt_0_succ. rewrite SF_ly_rev !SF_ly_f2 /= ?rev_cons. elim: P h => [ | h0 P IH] h //=. rewrite !rev_cons pairmap_rcons behead_rcons ?(IH h0) ?(Hf2 h h0) //. rewrite size_pairmap size_rcons ; apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy