proposition: Lemma CNF_simple_p1 a n b x: CNF_simple_ax a n b x -> ord_ext_div_pr omega0 x a (csucc n) b.
proof: Proof. move: OS_omega => oo [pa pb pc pd pe]. have csn := NS_succ pc. have osn:= OS_nat csn. split => //; split => //; first by apply/(oltP oo). apply: (ord_ne0_pos osn); apply: succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)