proposition: Lemma CNF_simple_exists x: \0o <o x -> exists a n b, CNF_simple_ax a n b x.
proof: Proof. move => xp. move: (ord_ext_div_exists ole_2omega xp) => [a [c [b [oa oc ob]]]]. move => [-> ha hb hc]; exists a, (cpred c), b. move /(oltP OS_omega): hb => cN. move: (cpred_pr cN (nesym (proj2 hc))) => [hd he]. by hnf; rewrite -he. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)