proposition: Lemma ord_factor9_aux k p: natp k -> (forall j, j <c k -> natp (p j)) -> (forall j, j <c k -> osuccp (p j)) -> posnatp (oprodf p k).
proof: Proof. move => kN ha hb. have: forall i, i <c k -> posnatp (p i). move => i lik; apply: (posnat_prop (ha _ lik)). move: (hb _ lik) => [m om -> ]. by move => ee; move:(succ_i m); rewrite ee => /in_set0. move: (k) kN; clear; apply:Nat_induction. move:olt_01 => h1 h2;rewrite oprod_f0; apply: PN1. move => n nN Hrec axi;rewrite (oprod_fS _ nN). move:(true_below_rec nN axi) => [/Hrec pn1 pn2]. by rewrite(oprod2_2int (proj1 pn1) (proj1 pn2)); apply: PN_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)