proposition: Lemma oprod_f1r p n: ord_below p (csucc n) -> natp n -> oprodf p (csucc n) = p \0c *o oprodf (fun i => p (csucc i)) n.
proof: Proof. move => obn nN. move:(obn _ (succ_positive n)) => op0. have ha: \1c +c n = csucc n by rewrite (Nsucc_rw nN) csumC. rewrite - ha in obn. rewrite - ha (oprod_fA NS1 nN obn) (oprod_f1 op0); apply: f_equal. by apply:(oprodf_exten nN) => i lin; rewrite -(Nsucc_rw (NS_lt_nat lin nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)