proposition: Lemma slist_append_val2 x y i: slistp x -> slistp y -> i<c slength y -> Vg (slist_append x y) ((slength x) +c i) = Vg y i.
proof: Proof. move => ha hb hc. move:(slength_nat ha)(slength_nat hb) => nN mN. have hi: inc (slength x +c i) (slength x +c slength y). by apply /(NltP (NS_sum nN mN)); apply:csum_Meqlt. have iN:=(NS_lt_nat hc mN). move:(Nsum_M0le i nN); rewrite {1} csumC => /cleNgt bad. by rewrite /slist_append (LgV hi) (csumC _ i) (cdiff_pr1 iN nN); Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)