proposition: Lemma least_cardinal2 (p : property): (forall b, natp b -> (forall x, x <c b -> p x) -> p b) -> forall a, natp a -> p a.
proof: Proof. move => H a aN. move: (OS_nat aN) => oa; move: a oa aN; apply: least_ordinal2. move => b ob Hb bN; apply:(H b bN) => x xlb. exact:(Hb x (oclt xlb) (NS_lt_nat xlb bN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)