proposition: Lemma ech_product_prop1 f g n m i (v:= ech_product1 f g n m): natp n -> natp m -> [/\ i <c n -> v i = (Vg f i), v(n +c m) = (J n (n +c m)) & i <c m -> v (n +c i) = ech_shift n (Vg g i)].
proof: Proof. rewrite /v /ech_product1 => nN mN. have ha k: ~(n +c k <c n) by apply/cleNgt; exact: (Nsum_M0le _ nN). split. - by move => lin; Ytac0. - by rewrite (Y_false (ha m)) Y_true. move => lim. rewrite (Y_false (ha i)); Ytac h. move: lim =>[lim];case; exact: (csum_eq2l nN (NS_le_nat lim mN) mN h). by rewrite csumC (cdiff_pr1 (NS_lt_nat lim mN) nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)