proposition: Lemma inaccessible_pr3 x: \2c <c x -> (forall f, cprod_of_small f x -> cprod f <c x) -> card_dominant x.
proof: Proof. move => cx h. have ccx := proj32_1 cx. apply: card_dominant_pr1 => //. move => p; rewrite p in cx; case: (clt0 cx). move => m mx; rewrite - cprod_of_same; apply: h; hnf; aw; split => //. hnf;aw => t te; rewrite LgV; fprops. by move => t te; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)