fact: Definition Rle_trans := λ"x" λ"y" λ"q" λ"q'" λ"z" average @ "q" @ "q'" @ (λ"q''" "y" @ "q''" @ "q'" @ ("x" @ "q" @ "q''" @ "z")).
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals