proposition: Lemma slist2_prop a b (c:= slist2 a b): [/\ slistpl c \2c, Vg c \0c = a & Vg c \1c = b].
proof: Proof. have fgE: fgraph c by apply: Lg_fgraph. have dE: domain c = \2c by exact: Lgd. have le: slistp c by split; [ exact | rewrite dE; exact NS2 ]. have sa:inc \1c \2c by apply /(NltP NS2); exact: clt_12. have sb:inc \0c \2c by apply /(NltP NS2); exact: clt_02. have sc:=card1_nz. by split => //;rewrite ?(LgV sa) ?(LgV sb); Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)