proposition: Lemma oprodf_exten f g n: natp n -> same_below f g n -> oprodf f n = oprodf g n.
proof: Proof. move: n; apply: Nat_induction. by move => _; rewrite ! oprod_f0. move => n nN Hrec /(true_below_rec nN) [/Hrec h1 h2]. by rewrite !(oprod_fS _ nN) h1 h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)