fact: Definition Ex4_10_hyp r n:= exists g A f, [/\ order_fam g, (allf g total_order), cardinal (domain g) = n , sub A (substrate (order_product g)) & order_isomorphism f r (induced_order (order_product g) A)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)