proposition: Lemma infinite_product_prop2 k (lo:= graph_on ord_pair_le (coarse k)) (f := ordinal_iso lo): infinite_c k -> bijection_prop f (product k k) k /\ (forall x y, inc x (source f) -> inc y (source f) -> (glt lo x y <-> (Vf f x) <o (Vf f y))).
proof: Proof. move => ik. have pa: (forall z, infinite_c z -> z <o k -> z *c z = z). by move =>z iz _ ; apply: infinite_product_alt. exact:(infinite_product_aux ik pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)