proposition: Lemma SF_lx_ly_inj (s s0 : SF_seq) : SF_lx s = SF_lx s0 -> SF_ly s = SF_ly s0 -> s = s0.
proof: Proof. move: s0 ; apply SF_cons_ind with (s := s) => {s} [x | h s IH] s0 ; apply SF_cons_dec with (s := s0) => {s0} [x0 | h0 s0] Hx Hy //. rewrite !SF_lx_nil in Hx. replace x with (head 0 ([::x])) by intuition ; by rewrite Hx. rewrite !SF_lx_cons in Hx ; rewrite !SF_ly_cons in Hy. replace h with (head (fst h) (fst h :: SF_lx s),head (snd h) (snd h :: SF_ly s)) ; [ rewrite Hx Hy (IH s0) //= | move => /= ; by apply injective_projections]. replace (SF_lx s) with (behead (fst h :: SF_lx s)) by intuition ; by rewrite Hx. replace (SF_ly s) with (behead (snd h :: SF_ly s)) by intuition ; by rewrite Hy. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy