proposition: Lemma infinite_prod_pA: cprodb Nat csucc = cprodb Nat (fun z => (csucc (csucc z))).
proof: Proof. set j := Nat -s1 \0c. set f := (Lg Nat csucc). have fgf: fgraph f by rewrite /f; fprops. have sj:sub j (domain f) by rewrite /f; aw;apply sub_setC. have sj1: sub (singleton \0c) Nat by move=> t /set1_P ->; apply:NS0. have f1: (forall i, inc i ((domain f) -s j) -> (Vg f i) = \1c). rewrite /f/j; aw => i /setC_P [iN] /setC_P nv; rewrite LgV//. rewrite - succ_zero; ex_middle aux; case: nv;split => //. by dneg i0; move /set1_P: i0 => ->. rewrite /cprodb (cprod_one_unit sj f1). have ->: cprodb j (Vg f) = cprodb j csucc. by rewrite /f;apply: cprodb_exten => i ii; rewrite LgV//; move/setC1_P: ii => []. apply:cprod_Cn2; split => //. + move => t tN; apply /setC_P;split; first by apply:NS_succ. move /set1_P; apply: succ_nz. + move => u v uN vN;apply: csucc_inj; fprops. + move => y /setC1_P [yn ynz]. by move: (cpred_pr yn ynz) => [pa pb]; exists (cpred y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)