proposition: Lemma slist6_prop a b c d e f (E:= slist6 a b c d e f): [/\ slistpl E \6c, Vg E \0c = a, Vg E \1c = b & [/\ Vg E \2c = c, Vg E \3c = d , Vg E \4c = e & Vg E \5c = f ]].
proof: Proof. move: NS0 NS1 NS2 NS3 NS4 NS5 NS6 => ns0 ns1 ns2 ns3 ns4 ns5 ns6. have fgE: fgraph E by apply: Lg_fgraph. have dE: domain E = \6c by exact: Lgd. have lE: slistp E by split => //; rewrite dE. move:(clt_6) => [l06 l16 l26 l36 [l46 l56]]. have i06: inc \0c \6c by apply/(NltP ns6). have i16: inc \1c \6c by apply/(NltP ns6). have i26: inc \2c \6c by apply/(NltP ns6). have i36: inc \3c \6c by apply/(NltP ns6). have i46: inc \4c \6c by apply/(NltP ns6). have i56: inc \5c \6c by apply/(NltP ns6). split => //. - by rewrite (LgV i06); Ytac0. - by rewrite (LgV i16) (Y_false(nesym (proj2 clt_01))); Ytac0. - split. - rewrite (LgV i26) (Y_false(nesym (proj2 clt_02))). by rewrite (Y_false(nesym (proj2 clt_12))); Ytac0. - move:clt_3 => [lt03 lt13 lt23]. rewrite (LgV i36) (Y_false(nesym (proj2 lt03))). rewrite (Y_false(nesym (proj2 lt13))). by rewrite (Y_false(nesym (proj2 lt23))); Ytac0. - move:clt_4 => [lt04 lt14 lt24 lt34]. rewrite (LgV i46) (Y_false(nesym (proj2 lt04))). rewrite (Y_false(nesym (proj2 lt14))). rewrite (Y_false(nesym (proj2 lt24))). by rewrite (Y_false(nesym (proj2 lt34))); Ytac0. - move:clt_5 => [lt05 lt15 lt25 lt35 lt45]. rewrite (LgV i56) (Y_false(nesym (proj2 lt05))). rewrite (Y_false(nesym (proj2 lt15))). rewrite (Y_false(nesym (proj2 lt25))). rewrite (Y_false(nesym (proj2 lt35))). by rewrite (Y_false(nesym (proj2 lt45))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)