(* Main properties **********************************************************)
theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
(* Main properties **********************************************************)
theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).