proposition: Lemma inaccessible_dominant3 x: omega0 <c x -> (inaccessible x <-> ( (forall a b, a <c x -> b <c x -> a ^c b <c x) /\ (forall z, \0c <c z -> z <c x -> x ^c z = x))).
proof: Proof. move => [h1 h2]. have ix: infinite_c x by apply /infinite_c_P2. move: (inaccessible_dominant2 x) => [pa pb pc pd]; split. move => h; move: (pd (or_intror h)) => [[_ pe] pf]; split => //. move => [h3 h4]. by case: (pc (conj ix h3) h4) => // eq; move: h2; rewrite eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)