proposition: Lemma slist_append_val1 x y i: slistp x -> slistp y -> i<c slength x -> Vg (slist_append x y) i = Vg x i.
proof: Proof. move => ha hb hc. move:(slength_nat ha)(slength_nat hb) => nN mN. have hi: inc i (slength x +c slength y). by apply /(NltP (NS_sum nN mN)); apply: (clt_leT hc); apply:Nsum_M0le. by rewrite /slist_append LgV //; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)