proposition: Lemma inaccessible_dominant x: inaccessible x -> card_dominant x.
proof: Proof. move => [[pa1 pa2] pb]. move: pa2 => [n [on _ _] xv]. move: (CIS_aleph on); rewrite - xv => icx. apply: (card_dominant_pr1 (proj1 icx) (infinite_nz icx) pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)