proposition: Lemma cnfp_shift_expo x d: cnfp x -> ordinalp d -> cnfp(cnf_shift_expo x d).
proof: Proof. rewrite/cnf_shift_expo; move => /cnfpP [ha hb hc hd] od; apply/cnfpP; split. - fprops. - by aw. - aw => i idx; rewrite LgV//; move:(hc _ idx) => [qa qb qc]; split; aww. - aw; move => i iN idx; move:(hd i iN idx) => lt1. move/(NltP hb): (clt_ltT (cltS iN) idx) => qa. move/(NltP hb): idx => idx. rewrite /oexp !LgV//; aw; apply: (osum_Meqlt lt1 od). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)