(* Note: this is the companion of lfxs_trans_fsle *)
theorem lfxs_trans_fsge: ∀R,R1,R2,R3.
                         lfxs_transitive_next R1 R R3 →
                         ∀L1,L,T. L1 ⪤*[R1, T] L →
                         ∀L2. L ⪤[R2] L2 → L1 ⪤*[R3, T] L2.
#R #R1 #R2 #R3 #HR #L1 #L #T #H
cases H -H #f1 #Hf1 #HL1 #L2 * #f #Hf #HL2
@(ex2_intro … Hf1) -Hf1
@(lexs_trans_gen … HL1) -HL1
[5: @(sle_lexs_conf … HL2) -HL2 /2 width=1 by sle_isid_sn/ |1,2: skip
|4: //
|3: