proposition: Lemma CNFp_A p n m : natp n -> natp m -> CNFp_ax1 p (n +c m) -> CNFpv1 p (n +c m) = (CNFpv1 p n) *o CNFpv1 (fun z => p (z +c n)) m.
proof: Proof. move => nN mN /OS_CNFp0; exact(oprod_fA nN mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)