proposition: Lemma ex4d_orderIr_prop3 (A:= \Po Nat): ex4_prop_IR (ex4d_orderI A)(ex4d_orderr A) /\ forall z, cofinal (ex4d_orderr A) z -> ~ countable_set z.
proof: Proof. move: (card_setP Nat) cardinal_Nat ; rewrite -/A => cA cN. have ccN: cardinalp Nat by rewrite - cN; fprops. have ucA: uncountable_set A. by move/countableP => /cleNgt []; move:(cantor ccN); rewrite - cA. split; first by apply:(ex4d_orderIr_prop1 (uncountable_set_infinite ucA)). move => z zcf zco; exact:(ex4d_orderIr_prop2 ucA zcf zco). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)