proposition: Lemma cnfpP x: cnfp x <-> [/\ fgraph x, natp (domain x), forall i, inc i (domain x) -> omonomp (Vg x i) & forall i, natp i -> (csucc i) <c (domain x) -> oexp x i <o oexp x (csucc i)].
proof: Proof. split; move => [ha hb hc hd]. move: hd => [[qa qb qc qd] qe]; split => //. move => i idx; move/(NltP hb): (idx) => lin. split; [ by apply: hc | by apply: qb | apply/ (posnat_ordinalp)]. exact: (conj (qe _ lin) (qc _ lin)). split => //; first by move => i /hc []. split => //. split. - apply: ole_2omega. - by move => i /(NltP hb) /hc[]. - by move => i /(NltP hb) /hc /proj33/posnat_ordinalp []. - exact. by move => i /(NltP hb) /hc /proj33/posnat_ordinalp []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)